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.

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: WF.GuessLex: If there is only one plausible measure, use it #2954

Merged
merged 40 commits into from
Nov 27, 2023
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
40 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
ee69575
feat: WF.GuessLex: If there is only one plausible measure, use it
nomeata Nov 23, 2023
2d9558d
Update test output
nomeata Nov 23, 2023
c157b6a
Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/gu…
nomeata Nov 24, 2023
0b3f5bb
Merge branch 'joachim/guess-lex' into joachim/guess-lex-shortcut
nomeata Nov 24, 2023
b33b524
Empty commit to trigger mathlib CI
nomeata Nov 24, 2023
bc6a394
Merge branch 'joachim/guess-lex' into joachim/guess-lex-shortcut
nomeata Nov 24, 2023
99cb590
Let’s just leave this here for now
nomeata Nov 24, 2023
56aaef6
Make sure tests are not unary non-mutual and really exercise GuessLex
nomeata Nov 27, 2023
79cf254
Fix test
nomeata Nov 27, 2023
4013a4b
Merge commit 'cbba783bcfd41651589f9823642a75594845eac8' into joachim/…
nomeata Nov 27, 2023
d74837e
Merge branch 'joachim/guess-lex' into joachim/guess-lex-shortcut
nomeata Nov 27, 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
Prev Previous commit
Next Next commit
Forgot one
  • Loading branch information
nomeata committed Nov 23, 2023
commit cd7fbd4aa08a8f92a79eec77a8e841fbc070c509
2 changes: 1 addition & 1 deletion src/Lean/Meta/CasesOn.lean
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
-- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
Expr.abstractM body fvs

/-- A non-failing version of `CasesOnApp.transform` -/
/-- A non-failing version of `CasesOnApp.refineThrough` -/
def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) :
MetaM (Option (Array Expr)) :=
try
Expand Down
2 changes: 1 addition & 1 deletion src/Lean/Meta/Match/Match.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1023,7 +1023,7 @@ def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array
-- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out
Expr.abstractM body fvs

/-- A non-failing version of `MatcherApp.transform` -/
/-- A non-failing version of `MatcherApp.refineThrough` -/
def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) :
MetaM (Option (Array Expr)) :=
try
Expand Down