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

feat: well-founded recursion #250

Merged
merged 32 commits into from
Jan 17, 2025
Merged

feat: well-founded recursion #250

merged 32 commits into from
Jan 17, 2025

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Jan 14, 2025

Closes #57

@nomeata nomeata changed the title Well-founded recursion feat: well-founded recursion Jan 14, 2025
@david-christiansen david-christiansen added the HTML available HTML has been generated for this PR label Jan 14, 2025
@github-actions github-actions bot temporarily deployed to lean-ref-pr-#250 January 14, 2025 12:06 Inactive
@github-actions github-actions bot temporarily deployed to lean-ref-pr-draft-#250 January 14, 2025 12:06 Inactive
@david-christiansen
Copy link
Collaborator

I'll wait until it's un-drafted to read the text. Thanks!

@nomeata nomeata added HTML available HTML has been generated for this PR and removed HTML available HTML has been generated for this PR labels Jan 14, 2025
@nomeata
Copy link
Collaborator Author

nomeata commented Jan 15, 2025

Ok, I think that’s a decent first iteration.

It is much less detailed on the internal construction than the structural recursion section, but think that’s ok, and the construction doesn’t have to be covered that prominently.

Please give it a read when you get to it, and either let me know what's missing (and I can write some more), or take it over get it into final shape, what works better for you.

It maybe be that I am not using Verso’s full potential when it comes to showing proofs states, I’ll watch your changes there and learn.

@nomeata
Revert "Local setup"
7a0ee06 
This reverts commit a8a57e8.
@nomeata nomeata marked this pull request as ready for review January 15, 2025 15:01
@nomeata nomeata removed the HTML available HTML has been generated for this PR label Jan 15, 2025
@nomeata nomeata added the HTML available HTML has been generated for this PR label Jan 16, 2025
nomeata
nomeata commented Jan 16, 2025
View reviewed changes
Manual/Language/RecursiveDefs/WF.lean Outdated Show resolved Hide resolved
Manual/Language/RecursiveDefs/WF.lean Outdated Show resolved Hide resolved
@david-christiansen
Copy link
Collaborator

All right, ball's back in your court. Thanks a ton!

@github-actions GitHub Actions
Copy link

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 13f917b.

@david-christiansen david-christiansen merged commit e674589 into leanprover:main Jan 17, 2025
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@david-christiansen david-christiansen david-christiansen left review comments

Assignees
No one assigned
Labels
HTML available HTML has been generated for this PR
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Describe well-founded recursion
2 participants
@nomeata @david-christiansen