From a8bb7fab93e84f00f06dc8d28251819e44fe455f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Mar 2022 12:12:43 -0700 Subject: [PATCH] fix: typo at `findRecArg` The code was not traversing the indices if the datatype has parameters --- src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index 62ab78ef48..0a4f5f7124 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -65,7 +65,7 @@ partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M /- If `e` is an inductive family, we store in `indicesRef` all variables in `xs` that occur in "index positions". -/ matchConstInduct e.getAppFn (fun _ => pure ()) fun info _ => do if info.numIndices > 0 && info.numParams + info.numIndices == e.getAppNumArgs then - for arg in e.getAppArgs[:info.numIndices] do + for arg in e.getAppArgs[info.numParams:] do forEachExpr arg fun e => do if e.isFVar && xs.any (· == e) then indicesRef.modify fun indices => indices.insert e.fvarId! @@ -74,6 +74,7 @@ partial def findRecArg (numFixed : Nat) (xs : Array Expr) (k : RecArgInfo → M let rec go (i : Nat) (firstPass : Bool) : M α := do if h : i < xs.size then let x := xs.get ⟨i, h⟩ + trace[Elab.definition.structural] "findRecArg x: {x}, firstPass: {firstPass}" let localDecl ← getFVarLocalDecl x if localDecl.isLet then throwStructuralFailed