max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: term info for inductive ctors

Browse source
This commit is contained in:
Gabriel Ebner 2022-09-14 14:45:25 +02:00 • committed by Leonardo de Moura
parent f1b5fa53f0
commit 10ff2601c5
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Inductive.lean
View file

@ -787,7 +787,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
for view in views do
Term.addTermInfo' view.ref[1] (← mkConstWithLevelParams view.declName) (isBinder := true)
for ctor in view.ctors do
Term.addTermInfo' ctor.ref[2] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
Term.addTermInfo' ctor.ref[3] (← mkConstWithLevelParams ctor.declName) (isBinder := true)
-- We need to invoke `applyAttributes` because `class` is implemented as an attribute.
Term.applyAttributesAt view.declName view.modifiers.attrs .afterTypeChecking