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

Reimplement primrec based on trees #16416

Open
wants to merge 37 commits into
base: master
Choose a base branch
from
Open

Reimplement primrec based on trees #16416

wants to merge 37 commits into from

Conversation

prakol16
Copy link
Collaborator

@prakol16 prakol16 commented Sep 7, 2022 •
edited

Open in Gitpod

TODO:

  • Write tactic to solve primrec goals
  • Equivalence between nat.primrec and primrec

@prakol16 prakol16 added the WIP Work in progress label Sep 7, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 7, 2022
@prakol16
Move primrec file
83c6d74
@prakol16
Fix duplicate instance arg
0b546fb
@prakol16
Add docstrings
4af6fbd
@prakol16
Merge branch 'tree_encoding' of https://github.com/leanprover-communi…
1104324 
…ty/mathlib into tree_primrec
@prakol16
Minor, docs
91a4893
@prakol16
Fix import
3673b4d
@prakol16
Add missing docstrings
d1de5f2
@prakol16
Merge branch 'tree_encoding' of https://github.com/leanprover-communi…
90ebe6a 
…ty/mathlib into tree_primrec
@prakol16
Start working on tactic
6d98d74
@prakol16
Primrec predicates
9bd67ca
@prakol16
Continue tactic, lemmas
f4b161a
@prakol16
Need to iterate to make the tactic faster
6be1432
@prakol16
Faster tactic, but why is it faster??
efcd243
@prakol16
Add more documentation to stack_recursion
448bf11
@prakol16
Use unit_tree instead of tree
baa7fff
@prakol16
Fix tencodable
d7e7a97
@prakol16
Merge branch 'tree_encoding' of https://github.com/leanprover-communi…
b861278 
…ty/mathlib into tree_primrec
@prakol16
Use unit_tree instead of tree unit
f4153de
@prakol16
More primrec
e36c4d7
@semorrison semorrison added not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 too-late This PR was ready too late for inclusion in mathlib3 and removed not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 labels Jul 16, 2023
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
blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. too-late This PR was ready too late for inclusion in mathlib3 WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@prakol16 @mathlib-dependent-issues-bot @semorrison