Documentation

Lean.Elab.PreDefinition.Structural.FindRecArg

Equations
partial def Lean.Elab.Structural.findRecArg.go {α : Type} (numFixed : Nat) (xs : Array Lean.Expr) (k : Lean.Elab.Structural.RecArgInfoLean.Elab.Structural.M α) (indices : Lean.FVarIdSet) (i : Nat) (firstPass : Bool) :