From 10ff2601c5b013c730d10f61bf165a82d7465d36 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 14 Sep 2022 14:45:25 +0200 Subject: [PATCH] fix: term info for inductive ctors --- src/Lean/Elab/Inductive.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index d29dddc4d5..2e5e22a1cd 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -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