Leonardo de Moura 4a69643858 fix: nontermination while generating equation lemmas for match-expressions (#6180) ... This PR fixes a non-termination bug that occurred when generating the match-expression equation theorems. The bug was triggered when the proof automation for the equation theorem repeatedly applied `injection(` to the same local declaration, as it could not be removed due to forward dependencies. See issue #6067 for an example that reproduces this issue. closes #6067		2024-11-23 00:06:34 +00:00
..
MatcherApp	feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)	2024-11-22 03:05:51 +00:00
Basic.lean	chore: move MessageData.ofConstName earlier (#5877)	2024-10-29 21:23:51 +00:00
CaseArraySizes.lean	feat: change Array.get to take a Nat and a proof (#6032)	2024-11-12 03:30:46 +00:00
CaseValues.lean	fix: match literal pattern support	2024-02-24 16:08:07 -08:00
Match.lean	feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)	2024-11-22 03:05:51 +00:00
MatchEqs.lean	fix: nontermination while generating equation lemmas for match-expressions (#6180)	2024-11-23 00:06:34 +00:00
MatchEqsExt.lean	fix: do not include internal match equational theorems at simp trace (#4274)	2024-05-25 17:16:19 +00:00
MatcherApp.lean	refactor: module MatcherApp.Transform (#3439)	2024-02-22 16:16:26 +00:00
MatcherInfo.lean	refactor: generalize addMatcherInfo (#5068)	2024-08-16 06:24:32 +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