New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Finish completeness of NbE #87

Closed

8 tasks done

Ailrun opened this issue May 21, 2024 · 0 comments · Fixed by #90

Milestone

Port NbE proof fr...

Member

Ailrun commented May 21, 2024 •

edited

Loading

Cases related to universes
- Prove some cases of completeness #74
- Change isomorphism between per_elem #81
Cases related to structures of term typing
- Prove some cases of completeness #74
- Change isomorphism between per_elem #81
Cases related to functions
- Change isomorphism between per_elem #81
- More completeness cases #84
Cases related to variables
Cases related to structures of substitutions
- More cases for completeness #88
Cases related to natural numbers
- More cases for completeness #88
- Finish completeness #90
Fundamental theorem
- Finish completeness #90
Main completeness theorem
- Finish completeness #90

This was referenced May 21, 2024

More cases for completeness #88

Merged

Finish completeness #90

Merged

Ailrun added this to the Port NbE proof from Agda to Coq milestone

Ailrun closed this as completed in #90

Ailrun changed the title ~~Finish Completeness~~ Finish Completeness of NbE

Ailrun changed the title ~~Finish Completeness of NbE~~ Finish completeness of NbE

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment