def
Lean.Elab.Structural.findRecArg
{α : Type}
(numFixed : Nat)
(xs : Array Lean.Expr)
(k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α)
:
Equations
- Lean.Elab.Structural.findRecArg numFixed xs k = do let indicesRef ← liftM (IO.mkRef ∅) let r ← forIn xs PUnit.unit fun x r => do let xType ← liftM (Lean.Meta.inferType x) liftM (Lean.Meta.forEachExpr xType fun e => Lean.matchConstInduct (Lean.Expr.getAppFn e) (fun x => pure ()) fun info x => if (decide (info.numIndices > 0) && info.numParams + info.numIndices == Lean.Expr.getAppNumArgs e) = true then do let r ← let col := Array.toSubarray (Lean.Expr.getAppArgs e) 0 info.numIndices; forIn col PUnit.unit fun arg r => do Lean.Meta.forEachExpr arg fun e => if (Lean.Expr.isFVar e && Array.any xs (fun a => a == e) 0 (Array.size xs)) = true then ST.Ref.modify indicesRef fun indices => Std.RBTree.insert indices (Lean.Expr.fvarId! e) else pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit else pure PUnit.unit) pure (ForInStep.yield PUnit.unit) let x : PUnit := r let indices ← ST.Ref.get indicesRef (fun go => go numFixed true) (Lean.Elab.Structural.findRecArg.go numFixed xs k indices)
partial def
Lean.Elab.Structural.findRecArg.go
{α : Type}
(numFixed : Nat)
(xs : Array Lean.Expr)
(k : Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α)
(indices : Lean.FVarIdSet)
(i : Nat)
(firstPass : Bool)
: