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

Revamp fixpoint code #49

Merged
merged 37 commits into from
Nov 26, 2024
Merged

Revamp fixpoint code #49

merged 37 commits into from
Nov 26, 2024

Conversation

jvanbruegge
Copy link
Owner

ISSUES FIXED: #40

@jvanbruegge jvanbruegge force-pushed the fixpoint-revamp branch 3 times, most recently from 7b84424 to eb2ab48 Compare August 8, 2024 13:48
@jvanbruegge jvanbruegge force-pushed the fixpoint-revamp branch 2 times, most recently from 6e968b5 to 40b177c Compare August 17, 2024 10:29
@jvanbruegge jvanbruegge force-pushed the fixpoint-revamp branch 2 times, most recently from f381b6f to 3cad382 Compare August 28, 2024 13:34
@jvanbruegge jvanbruegge force-pushed the fixpoint-revamp branch 3 times, most recently from 7c3fcbb to f878c1e Compare October 15, 2024 14:04
@jvanbruegge
Add operations theory for least fixpoint
1ac8a6f
@jvanbruegge
Adapt recursor operations to manual fixpoint theory
a80e591
@jvanbruegge
Add bound free position to fixpoint operation
94fd68c
@jvanbruegge
Adapt recursor operations theory for bound free
ba4173b
@jvanbruegge
Allow to disable noting of mrbnf theorems
c10476b
@jvanbruegge
Reorder fixpoint operations theory to bundle definitions
b2a2c20
@jvanbruegge
Add @{map_filter n} antiquotation
bbc0f9b
@jvanbruegge
Rename old fixpoint code
a129e9a
@jvanbruegge
Define fixpoint constants from ML
d070240
@jvanbruegge
Automate fixpoint theorems up to and including alpha_trans
834b39e
@jvanbruegge
Fix equivp subgoals for quotient
2295954
@jvanbruegge
Add operations theory for two datatype with two binding position for …
62e2ade 
…one free position
@jvanbruegge
Note covar_large theorem properly in covar class
e3f02a7
@jvanbruegge
Add more lemmas about id_on and eq_on
d32750b
@jvanbruegge
Add operations theory for greatest fixpoint
71af052
@jvanbruegge
Use same tactic for alpha_FVars for codatatypes and datatypes
135e793
@jvanbruegge
Remove usage of subgoal_tac, hard to use from ML
90fdbf8
@jvanbruegge
Use induction on free vars for alpha_FVars in lfp operations
6df6526
@jvanbruegge jvanbruegge force-pushed the fixpoint-revamp branch 2 times, most recently from 65dd913 to dbb22f2 Compare October 18, 2024 10:28
@jvanbruegge jvanbruegge marked this pull request as ready for review November 19, 2024 14:50
@jvanbruegge jvanbruegge merged commit 1ebcefd into master Nov 26, 2024
1 check passed
@jvanbruegge jvanbruegge deleted the fixpoint-revamp branch November 26, 2024 14:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Allow to bind in other things not just in recursive positions
1 participant
@jvanbruegge