yiyunliu/pair-eta
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
No description
92 commits 16 branches 0 tags 433 KiB
Coq 99.2%
Makefile 0.5%
Standard ML 0.3%
Find a file
Exact
Yiyun Liu 9c17ec5cac Start refactoring to unscoped syntax
2025-04-01 23:21:39 -04:00
theories Start refactoring to unscoped syntax 2025-04-01 23:21:39 -04:00
.gitignore Initial commit 2024-12-11 23:52:57 -05:00
_CoqProject Initial commit 2024-12-11 23:52:57 -05:00
Makefile Start refactoring to unscoped syntax 2025-04-01 23:21:39 -04:00
README.md Create README.md 2024-12-25 21:15:48 -05:00
syntax.sig Rename the term constructors 2025-01-24 14:52:35 -07:00

README.md

This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.