yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add ci

Browse source
This commit is contained in:
Yiyun Liu 2025-04-28 17:33:12 -04:00
parent 0e04a7076b
commit d7207c6532
2 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
.woodpecker.yaml Normal file
View file

@ -0,0 +1,13 @@
when:
- event: [push, pull_request]
branch: [main]
steps:
- name: build
image: coqorg/coq:8.20.1-ocaml-4.14.2-flambda
commands:
- opam update
- opam install -y coq-hammer-tactics coq-equations coq-stdpp coq-autosubst-ocaml
- eval $(opam env)
- sudo chown -R 1000:1000 .
- make -j2

2
README.org
View file

@ -1,4 +1,6 @@
* Church Rosser, surjective pairing, and strong normalization * Church Rosser, surjective pairing, and strong normalization
[![status-badge](https://woodpecker.electriclam.com/api/badges/3/status.svg)](https://woodpecker.electriclam.com/repos/3)
This repository contains a mechanized proof that the lambda calculus This repository contains a mechanized proof that the lambda calculus
with beta and eta rules for functions and pairs is in fact confluent with beta and eta rules for functions and pairs is in fact confluent
for the subset of terms that are "strongly $\beta$-normalizing". for the subset of terms that are "strongly $\beta$-normalizing".