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

feat: Guess lexicographic order for well-founded recursion #2874

Merged
merged 32 commits into from
Nov 27, 2023
Merged

feat: Guess lexicographic order for well-founded recursion #2874

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
a2d5d94
feat: Guess lexicographic order for well-founded recursion
nomeata Nov 14, 2023
ea171dc
Use same error message as before
nomeata Nov 14, 2023
0414156
Avoid overshooting in lambdaTelescope in matchers/casesOn
nomeata Nov 14, 2023
01f9968
feat: Add MatcherApp. and CasesOnApp.transform
nomeata Nov 15, 2023
a117d02
Use forallTelescope
nomeata Nov 16, 2023
338a239
Improve documentation, also for existing code
nomeata Nov 16, 2023
9c1b76b
Refactor stuff arount .transfer
nomeata Nov 15, 2023
dd26a05
Avoid TermElabM where MetaM suffices
nomeata Nov 15, 2023
b741f14
More comments
nomeata Nov 15, 2023
9252151
Less TermElabM
nomeata Nov 15, 2023
c514fa3
Code walkthrough with Sebastian
nomeata Nov 15, 2023
e8b6cb3
Use forallTelescope
nomeata Nov 16, 2023
9e3db47
Use forallTelescope
nomeata Nov 18, 2023
d0b5a26
Tuple syntax, forallTelescope
nomeata Nov 18, 2023
6d17de5
Docstring all the functions
nomeata Nov 20, 2023
2f04011
Change copyright
nomeata Nov 21, 2023
9321b8a
Merge branch 'joachim/transform' into joachim/guess-lex
nomeata Nov 23, 2023
6f7165a
Clean-up pass
nomeata Nov 23, 2023
5611e58
Apply review comments
nomeata Nov 23, 2023
815891d
Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/tr…
nomeata Nov 23, 2023
3e0f14c
Merge branch 'joachim/transform' into joachim/guess-lex
nomeata Nov 23, 2023
cd7fbd4
Forgot one
nomeata Nov 23, 2023
da93cc9
Merge branch 'joachim/transform' into joachim/guess-lex
nomeata Nov 23, 2023
069da84
.transform got renamed
nomeata Nov 23, 2023
4299967
Docstring
nomeata Nov 23, 2023
768c532
Apply review comments
nomeata Nov 23, 2023
f4f64e5
Remove old guessing code
nomeata Nov 23, 2023
64a8074
Add test cases
nomeata Nov 23, 2023
40fcd73
Factor out generateMeasures
nomeata Nov 23, 2023
c157b6a
Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/gu…
nomeata Nov 24, 2023
b33b524
Empty commit to trigger mathlib CI
nomeata Nov 24, 2023
99cb590
Let’s just leave this here for now
nomeata Nov 24, 2023
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