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

refactor: FunInd overhaul #4789

Merged
merged 20 commits into from
Jul 21, 2024
Merged

refactor: FunInd overhaul #4789

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
34bcf52
Stash refactor foldAndCollect
nomeata Jul 18, 2024
68b5cf9
Start merging foldAndCollect
nomeata Jul 18, 2024
050745f
Handle matcher app
nomeata Jul 18, 2024
ff9172e
Some fixes, test suite mostly passes now
nomeata Jul 18, 2024
2116339
More monadic handling of IHs
nomeata Jul 19, 2024
9f62eaf
Factor out isRecCall
nomeata Jul 19, 2024
1fec6e9
Comment
nomeata Jul 19, 2024
775e605
Start splitting wf support
nomeata Jul 19, 2024
f7b0014
Post-refactor cleanup
nomeata Jul 19, 2024
76325df
For structural
nomeata Jul 19, 2024
6a6862a
Catch mutual recursion earler
nomeata Jul 19, 2024
b3cdb69
Always use binductionOn
nomeata Jul 19, 2024
391ae08
Cleanup
nomeata Jul 19, 2024
6937ae9
Comments
nomeata Jul 19, 2024
f3f382b
Move functions
nomeata Jul 19, 2024
f9e993c
Update comment
nomeata Jul 19, 2024
11117ac
Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/fu…
nomeata Jul 19, 2024
ea9804b
Merge branch 'master' of github.com:leanprover/lean4 into joachim/fun…
nomeata Jul 19, 2024
314a224
Merge branch 'nightly-with-mathlib' of github.com:leanprover/lean4 in…
nomeata Jul 21, 2024
2c1e303
Remove unused functions
nomeata Jul 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading