doc: add comment about pattern LHS info nesting

leanprover · Sep 29, 2022 · 83a9728 · 83a9728
1 parent e6c70a3
commit 83a9728
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
@@ -321,6 +321,8 @@ where
           if altVars.size > numFieldsToName then
             logError m!"too many variable names provided at alternative '{altName}', #{altVars.size} provided, but #{numFieldsToName} expected"
           let mut (fvarIds, altMVarId) ← altMVarId.introN numFields (altVars.toList.map getNameOfIdent') (useNamesForExplicitOnly := !altHasExplicitModifier altStx)
+          -- Delay adding the infos for the pattern LHS because we want them to nest
+          -- inside tacticInfo for the current alternative (in `evalAlt`)
           let addInfo := do
             if (← getInfoState).enabled then
               if let some declName := declName? then