This commit is contained in:
parent
fe88b519a9
commit
4c527c1b81
1 changed files with 1 additions and 1 deletions
|
@ -1,5 +1,5 @@
|
|||
* Church Rosser, surjective pairing, and strong normalization
|
||||
[](https://woodpecker.electriclam.com/repos/3)
|
||||
[[https://woodpecker.electriclam.com/api/badges/3/status.svg]]
|
||||
|
||||
This repository contains a mechanized proof that the lambda calculus
|
||||
with beta and eta rules for functions and pairs is in fact confluent
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue