max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Leonardo de Moura adc45d7c7b
feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 
This PR marks any exposed (non-private) auxiliary match declaration as
`[implicit_reducible]`. This is essential when the outer declaration is
marked as `instance_reducible` — without it, reduction is blocked at the
match auxiliary. We do not inherit the attribute from the parent
declaration because match auxiliary declarations are reused across
definitions, and the reducibility setting of the parent can change
independently. This change prepares for implementing the TODO at
`ExprDefEq.lean:465`, which would otherwise cause too many failures
requiring manual `[implicit_reducible]` annotations on match
declarations whose names are not necessarily derived from the outer
function.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-04-04 23:55:47 +00:00
..
ArgsPacker
Constructions refactor: make exportEntriesFnEx return all olean levels at once (#13142) 2026-03-27 08:57:45 +00:00
DiscrTree chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Match feat: mark exposed match auxiliary declarations as implicit_reducible (#13281) 2026-04-04 23:55:47 +00:00
Sym feat: add mkAppNS, mkAppRevS, betaRevS, betaS, and related Sym functions (#13273) 2026-04-04 02:31:16 +00:00
Tactic chore: fix spelling errors (#13274) 2026-04-04 07:34:34 +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 chore: do not rely on Name.lt for ordering fvars in acLt (#12306) 2026-02-08 14:25:31 +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 perf: prevent unnecessary allocations of EST.Out.ok (#13163) 2026-03-27 22:10:24 +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 structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +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 feat: sparse sparse casesOn splitting in match equations (#11666) 2025-12-14 14:59:45 +00:00
CtorIdxHInj.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
CtorRecognizer.lean
DecLevel.lean
Diagnostics.lean
DiscrTree.lean refactor: DiscrTree (#11875) 2026-01-02 19:53:45 +00:00
Eqns.lean feat: allow deprecating options (#13195) 2026-04-02 14:44:11 +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: theorems are opaque (#12973) 2026-03-23 13:57:07 +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 chore: rename Substring to Substring.Raw (#11154) 2025-11-16 09:30:04 +00:00
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: rename instance_reducible to implicit_reducible (#12567) 2026-02-18 22:19:16 +00:00
IntInstTesters.lean fix: nonstandard instances in grind and simp +arith (#11758) 2025-12-21 17:56:49 +00:00
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 fix: add checkSystem calls to hasAssignableMVar (#13219) 2026-03-31 19:27:15 +00:00
LitValues.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Match.lean
MatchUtil.lean refactor: make MatchEqs a leaf module (#11493) 2025-12-03 09:15:36 +00:00
MethodSpecs.lean refactor: DiscrTree (#11875) 2026-01-02 19:53:45 +00:00
MkIffOfInductiveProp.lean chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
MonadSimp.lean refactor: have telescope support (#11914) 2026-01-06 19:20:25 +00:00
NatInstTesters.lean fix: nonstandard instances in grind and simp +arith (#11758) 2025-12-21 17:56:49 +00:00
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 chore: do not set unused Option.Decl.group (#11307) 2025-11-21 16:44:38 +00:00
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 perf: bypass typeclass synthesis in SizeOf spec theorem generation (#12849) 2026-03-09 15:08:48 +00:00
Sorry.lean chore: deprecate levelZero and levelOne (#12720) 2026-03-04 01:03:08 +00:00
SplitSparseCasesOn.lean feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
StringLitProof.lean perf: optimize string literal equality simprocs for kernel efficiency (#12887) 2026-03-14 10:30:31 +00:00
Structure.lean refactor: DiscrTree (#11875) 2026-01-02 19:53:45 +00:00
Sym.lean refactor: replace grind canonicalizer with type-directed normalizer (#13166) 2026-03-28 02:43:22 +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 chore: rename String.ValidPos to String.Pos (#11240) 2025-11-24 16:40:21 +00:00
UnificationHint.lean feat: add structured TraceResult to TraceData (#12698) 2026-03-10 02:42:57 +00:00
WHNF.lean fix: add checkSystem calls to long-running elaboration paths (#13220) 2026-04-01 12:54:57 +00:00
WrapInstance.lean doc: update inferInstanceAs docstring and rename normalizeInstance to wrapInstance (#13115) 2026-03-25 02:20:49 +00:00