lean4-htt/src/Lean/Meta/Match
Leonardo de Moura 0684c95d35
fix: do not lift (<- ...) over pure if-then-else (#3820)
Now, only `(<- ...)`s occurring in the condition of a pure if-then-else
are lifted.
That is, `if (<- foo) then ... else ...` is ok, but `if ... then (<-
foo) else ...` is not. See #3713

closes #3713 

This PR also adjusts this repo. Note that some of the `(<- ...)` were
harmless since they were just accessing some
read-only state.
2024-04-01 21:33:59 +00:00
..
MatcherApp fix: do not lift (<- ...) over pure if-then-else (#3820) 2024-04-01 21:33:59 +00:00
Basic.lean fix: match literal pattern support 2024-02-24 16:08:07 -08:00
CaseArraySizes.lean chore: missing double backticks (#3587) 2024-03-04 03:02:35 +00:00
CaseValues.lean fix: match literal pattern support 2024-02-24 16:08:07 -08:00
Match.lean fix: match-expression when patterns cover all cases of a BitVec finite type (#3538) 2024-02-29 02:24:47 +00:00
MatchEqs.lean fix: matcher splitter is code (#3815) 2024-04-01 02:14:14 +00:00
MatchEqsExt.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MatcherApp.lean refactor: module MatcherApp.Transform (#3439) 2024-02-22 16:16:26 +00:00
MatcherInfo.lean refactor: module MatcherApp.Transform (#3439) 2024-02-22 16:16:26 +00:00
MatchPatternAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
MVarRenaming.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Value.lean fix: match literal pattern support 2024-02-24 16:08:07 -08:00