Leonardo de Moura 8ebd294673 fix: kernel projection panic in Sym.simp match reduction (#13635) ... This PR fixes a `Sym.simp` panic ("unexpected kernel projection term during simplification") that triggered when matcher iota-reduction exposed kernel `Expr.proj` terms via struct-eta. For example, a `do` block with a `for` loop whose state is a tuple, where `Sym.simp` unfolds the equational lemma and then descends into a destructuring match.		2026-05-05 03:20:20 +00:00
..
ArgsPacker
Constructions	feat: add linter.redundantVisibility for redundant private/public modifiers (#13132)	2026-04-13 08:34:20 +00:00
DiscrTree	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Match	feat: add linter.redundantVisibility for redundant private/public modifiers (#13132)	2026-04-13 08:34:20 +00:00
Sym	fix: kernel projection panic in Sym.simp match reduction (#13635)	2026-05-05 03:20:20 +00:00
Tactic	fix: kernel projection panic in Sym.simp match reduction (#13635)	2026-05-05 03:20:20 +00:00
AbstractMVars.lean	feat: use StateT.run instead of function application (#5121)	2026-03-03 03:12:26 +00:00
AbstractNestedProofs.lean	fix: add checkSystem calls to long-running elaboration paths (#13220)	2026-04-01 12:54:57 +00:00
ACLt.lean	fix: prevent a hang in acLt (#13367)	2026-04-17 21:46:29 +00:00
AppBuilder.lean	fix: add checkSystem calls to hasAssignableMVar (#13219)	2026-03-31 19:27:15 +00:00
ArgsPacker.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Basic.lean	doc: note TransparencyMode and ReducibilityStatus constructors are not in unfolding order (#13564)	2026-04-29 04:22:55 +00:00
BinderNameHint.lean
Canonicalizer.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
CasesInfo.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Check.lean	feat: add .instances-transparency type-check diagnostics (#13368)	2026-05-02 12:17:51 +00:00
CheckTactic.lean
Closure.lean	feat: unfold and rewrap instances in inferInstanceAs and deriving	2026-03-22 13:25:46 +01:00
Coe.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
CoeAttr.lean
CollectFVars.lean
CollectMVars.lean
CompletionName.lean
CongrTheorems.lean	fix: use isClass? instead of binder annotation to identify instance parameters (#12172)	2026-01-28 20:33:43 +00:00
Constructions.lean
CtorIdxHInj.lean	feat: add linter.redundantVisibility for redundant private/public modifiers (#13132)	2026-04-13 08:34:20 +00:00
CtorRecognizer.lean
DecLevel.lean	fix: universe normalization in getDecLevel (#13391)	2026-04-14 21:27:22 +00:00
Diagnostics.lean
DiscrTree.lean
Eqns.lean	feat: add @[backward_defeq] attribute and local useBackward simp option (#13492)	2026-04-27 10:07:59 +00:00
Eval.lean	feat: stricter meta check for temporary programs in native_decide etc (#13005)	2026-03-20 15:51:18 +00:00
ExprDefEq.lean	feat: add backward.isDefEq.respectTransparency.types option (#13280)	2026-04-04 18:05:33 +00:00
ExprLens.lean
ExprTraverse.lean
ForEachExpr.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
FunInfo.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
GeneralizeTelescope.lean
GeneralizeVars.lean
GetUnfoldableConst.lean	feat: use explicit allowlist instead of transparency bump in whnfMatcher (#13363)	2026-04-24 13:50:30 +00:00
HasAssignableMVar.lean	feat: pretty print level metavariables using index (#13030)	2026-04-01 22:34:29 +00:00
HasNotBit.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
HaveTelescope.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Hint.lean
IndPredBelow.lean	feat: add structured TraceResult to TraceData (#12698)	2026-03-10 02:42:57 +00:00
Inductive.lean
InferType.lean	perf: add checkInterrupted to inferType cache miss path (#13258)	2026-04-03 06:03:55 +00:00
Injective.lean	feat: add structured TraceResult to TraceData (#12698)	2026-03-10 02:42:57 +00:00
Instances.lean	refactor: align ScopedEnvExtension.exportEntry? with new PersistentEnvExtension.exportEntriesFn (#13628)	2026-05-04 15:35:59 +00:00
IntInstTesters.lean
Iterator.lean
KAbstract.lean
KExprMap.lean
LazyDiscrTree.lean	refactor: remove unnecessary use of constNames in LazyDiscrTree (#12422)	2026-02-12 23:52:48 +00:00
LetToHave.lean	feat: add structured TraceResult to TraceData (#12698)	2026-03-10 02:42:57 +00:00
LevelDefEq.lean	feat: have level metavariable pretty printer instantiate level metavariables (#13438)	2026-04-18 01:07:22 +00:00
LitValues.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Match.lean
MatchUtil.lean
MethodSpecs.lean
MkIffOfInductiveProp.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
MonadSimp.lean
NatInstTesters.lean
Native.lean	chore: fix spelling errors (#13274)	2026-04-04 07:34:34 +00:00
NatTable.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Offset.lean	refactor: replace grind canonicalizer with type-directed normalizer (#13166)	2026-03-28 02:43:22 +00:00
Order.lean
PPGoal.lean
PProdN.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
ProdN.lean	feat: new, extensible do elaborator (#12459)	2026-02-21 17:17:29 +00:00
RecExt.lean	refactor: use isRecursiveDefinition when validating macro_inline (#12106)	2026-01-22 16:31:34 +00:00
RecursorInfo.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
Reduce.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
ReduceEval.lean
SameCtorUtils.lean	chore: fix spelling errors (#13274)	2026-04-04 07:34:34 +00:00
SizeOf.lean	fix: generate SizeOf spec theorems for inductives with private constructors (#13374)	2026-04-12 12:00:51 +00:00
Sorry.lean	chore: deprecate levelZero and levelOne (#12720)	2026-03-04 01:03:08 +00:00
SplitSparseCasesOn.lean	feat: add linter.redundantVisibility for redundant private/public modifiers (#13132)	2026-04-13 08:34:20 +00:00
StringLitProof.lean	perf: optimize string literal equality simprocs for kernel efficiency (#12887)	2026-03-14 10:30:31 +00:00
Structure.lean
Sym.lean	feat: add Sym.Arith infrastructure for arithmetic normalization (#13289)	2026-04-06 05:21:09 +00:00
SynthInstance.lean	perf: mark ReaderT context argument as borrow (#12942)	2026-03-23 14:45:52 +00:00
Tactic.lean	feat: add experimental cbv tactic (#12279)	2026-02-04 14:39:39 +00:00
Transform.lean	fix: add checkSystem calls to long-running elaboration paths (#13220)	2026-04-01 12:54:57 +00:00
TransparencyMode.lean	chore: shake core (#12276)	2026-02-05 09:10:32 +00:00
TryThis.lean
UnificationHint.lean	feat: add structured TraceResult to TraceData (#12698)	2026-03-10 02:42:57 +00:00
WHNF.lean	feat: use explicit allowlist instead of transparency bump in whnfMatcher (#13363)	2026-04-24 13:50:30 +00:00
WrapInstance.lean	feat: detect further sub-instances in wrapInstance (#13536)	2026-05-02 11:55:04 +00:00