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

Get rid of indefinite description and propositional extensionality #51

Closed

HuStmpHrrr opened this issue May 3, 2024 · 1 comment

Assignees

Milestone

Port NbE proof fr...

Member

HuStmpHrrr commented May 3, 2024

I think I just thought of a way to do it, but I actually need to put it down to see if it's actually the case.

HuStmpHrrr mentioned this issue

attempt to remove unnecessary axioms #52

Merged

HuStmpHrrr self-assigned this

HuStmpHrrr closed this as completed

Member

Ailrun commented May 4, 2024

BTW by mentioning an issue with "Closes"/"Fixes"/"Resolves"/... in a PR, you can auto-close the issue when the PR is merged.
(For example, as in #43)

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

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