Skip to content
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

Change isomorphism between per_elem #81

Merged
merged 10 commits into from
May 17, 2024
Merged

Change isomorphism between per_elem #81

merged 10 commits into from
May 17, 2024

Conversation

Ailrun
Copy link
Member

@Ailrun Ailrun commented May 15, 2024 •
edited
Loading

Surprisingly, per_univ_elem_cumu is still short (almost does not change at all in fact)

@HuStmpHrrr
Copy link
Member

use this PR to keep track of blockers, if any. (I am hoping not, as thinking about it right now, it is actually quite natural)

@Ailrun Ailrun changed the title [WIP] Change isomorphism between per_elem Change isomorphism between per_elem May 17, 2024
@Ailrun
Copy link
Member Author

Ailrun commented May 17, 2024

Now proofs are fully converted

@Ailrun Ailrun force-pushed the pr-use-different-iso branch from ef083a6 to 542529f Compare May 17, 2024 11:49
@HuStmpHrrr
Copy link
Member

I see that it's no longer WIP. let's review this PR and merge it first before adding more cases.

@HuStmpHrrr HuStmpHrrr merged commit 30d99cf into main May 17, 2024
2 checks passed
@HuStmpHrrr HuStmpHrrr deleted the pr-use-different-iso branch May 17, 2024 22:28
@Ailrun Ailrun mentioned this pull request May 21, 2024
Closed
8 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@HuStmpHrrr HuStmpHrrr HuStmpHrrr left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
Port NbE proof from Agda to Coq
Development

Successfully merging this pull request may close these issues.
2 participants
@Ailrun @HuStmpHrrr