Joachim Breitner 6995f280b4 fix: unfold abstracted proofs before processing recursion (#9191) ... This PR lets the equation compiler unfold abstracted proofs again if they would otherwise hide recursive calls. This fixes #8939. --------- Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>		2025-07-25 08:00:57 +00:00
..
ArgsPacker
Constructions	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
Match	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
Tactic	fix: kernel deep recursion with normalizer (#9522)	2025-07-25 04:37:17 +00:00
AbstractMVars.lean	feat: add the nondep field of Expr.letE to the C++ data model (#8751)	2025-06-14 23:10:27 +00:00
AbstractNestedProofs.lean	feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804)	2025-06-22 21:54:57 +00:00
ACLt.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
AppBuilder.lean	feat: eliminate letFun support, deprecate let_fun syntax (#9086)	2025-06-30 02:10:18 +00:00
ArgsPacker.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Basic.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
BinderNameHint.lean	chore: fix spelling mistakes (#7328)	2025-04-07 01:15:48 +00:00
Canonicalizer.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Check.lean	fix: reorder "application type mismatch" message (#9287)	2025-07-15 19:20:18 +00:00
CheckTactic.lean
Closure.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
Coe.lean	doc: add documentation for builtin attributes (#8173)	2025-06-11 09:04:37 +00:00
CoeAttr.lean
CollectFVars.lean
CollectMVars.lean	refactor: migrate all usages of old slice notation (#9000)	2025-06-27 18:52:07 +00:00
CompletionName.lean
CongrTheorems.lean	fix: mkCongrSimpCore? (#9472)	2025-07-22 18:09:24 +00:00
Constructions.lean
CtorRecognizer.lean
DecLevel.lean	chore: simproc and helper theorems for grind (#9151)	2025-07-02 03:57:12 +00:00
Diagnostics.lean	fix: show kernel diagnostics even for examples (#9509)	2025-07-24 09:21:47 +00:00
DiscrTree.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
DiscrTreeTypes.lean
Eqns.lean	feat: transform nondependent lets into haves in declarations and equation lemmas (#8373)	2025-06-29 19:45:45 +00:00
Eval.lean	refactor: introduce VisibilityMap in Lean.Environment, use it to split base in preparation for private import (#8145)	2025-04-28 10:17:18 +00:00
ExprDefEq.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
ExprLens.lean	feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804)	2025-06-22 21:54:57 +00:00
ExprTraverse.lean
ForEachExpr.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
FunInfo.lean	fix: let the congr tactic handle "under-applied" applications (#9225)	2025-07-08 11:48:08 +00:00
GeneralizeTelescope.lean
GeneralizeVars.lean
GetUnfoldableConst.lean	fix: unknown identifier ranges (#8362)	2025-05-22 10:05:31 +00:00
GlobalInstances.lean
Hint.lean	feat: add named argument hints (#9315)	2025-07-17 03:22:25 +00:00
IndPredBelow.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Inductive.lean
InferType.lean	perf: isArrowProposition (#9414)	2025-07-17 04:12:15 +00:00
Injective.lean	refactor: migrate all usages of old slice notation (#9000)	2025-06-27 18:52:07 +00:00
Instances.lean	refactor: remove Lean.RBMap usages (#9260)	2025-07-21 14:04:45 +00:00
IntInstTesters.lean	refactor: support for Nat in grind cutsat (#9340)	2025-07-13 23:40:03 +00:00
Iterator.lean
KAbstract.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
KExprMap.lean
LazyDiscrTree.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
LetToHave.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
LevelDefEq.lean
LitValues.lean	chore: remove prime from Fin.ofNat' (#8515)	2025-05-28 11:51:00 +00:00
Match.lean
MatchUtil.lean
NatInstTesters.lean
Offset.lean
Order.lean	chore: fix spelling mistakes (#8324)	2025-05-14 06:52:16 +00:00
PPGoal.lean	feat: use nondep flag in Expr.letE and LocalContext.ldecl (#8804)	2025-06-22 21:54:57 +00:00
PProdN.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
RecursorInfo.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
Reduce.lean	refactor: migrate to new ranges (#8841)	2025-07-07 12:41:53 +00:00
ReduceEval.lean
SizeOf.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
Sorry.lean
Structure.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
SynthInstance.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
Tactic.lean	feat: extract_lets and lift_lets tactics (#6432)	2025-04-21 08:57:01 +00:00
Transform.lean	fix: unfold abstracted proofs before processing recursion (#9191)	2025-07-25 08:00:57 +00:00
TransparencyMode.lean
TryThis.lean	chore: fix spelling errors (#9175)	2025-07-24 23:35:32 +00:00
UnificationHint.lean
WHNF.lean	chore: revert DefEq changes until it has passed proper review (#9254)	2025-07-08 14:54:18 +00:00