Support for collecting function calls that could be used for fun_induction or fun_cases. Used by fun_induction foo, and the Calls structure is also used by try?.

structure Lean.Meta.FunInd.Call : Type

• expr : Expr
• relevantArgs : Expr

def Lean.Meta.FunInd.instHashableCall.hash : Call → UInt64

@[implicit_reducible]

instance Lean.Meta.FunInd.instHashableCall : Hashable Call

def Lean.Meta.FunInd.instBEqCall.beq : Call → Call → Bool

@[implicit_reducible]

instance Lean.Meta.FunInd.instBEqCall : BEq Call

structure Lean.Meta.FunInd.SeenCalls : Type

• calls : Array Expr

  the full calls

• seen : Std.HashSet (Name × Array Expr)

  only function name and relevant arguments

@[implicit_reducible]

instance Lean.Meta.FunInd.instEmptyCollectionSeenCalls : EmptyCollection SeenCalls

def Lean.Meta.FunInd.SeenCalls.isEmpty (sc : SeenCalls) : Bool

def Lean.Meta.FunInd.SeenCalls.push (e : Expr) (funIndInfo : FunIndInfo) (args : Array Expr) (calls : SeenCalls) : MetaM SeenCalls

def Lean.Meta.FunInd.SeenCalls.uniques (calls : SeenCalls) : NameSet

Which functions have exactly one candidate application. Used by try? to determine whether we can use fun_induction foo or need fun_induction foo x y z.

@[reducible, inline]

abbrev Lean.Meta.FunInd.Collector.M (α : Type) : Type

def Lean.Meta.FunInd.Collector.saveFunInd (e : Expr) (funIndInfo : FunIndInfo) (args : Array Expr) : M Unit

def Lean.Meta.FunInd.Collector.visitApp (e : Expr) (funIndInfo : FunIndInfo) (args : Array Expr) : M Unit

@[reducible, inline]

unsafe abbrev Lean.Meta.FunInd.Collector.Cache : Type

unsafe def Lean.Meta.FunInd.Collector.visit (e : Expr) : StateRefT' IO.RealWorld Cache M Unit

unsafe def Lean.Meta.FunInd.Collector.main (needle : FunIndInfo) (mvarId : MVarId) : MetaM (Array Expr)

def Lean.Meta.FunInd.collect (needle : FunIndInfo) (mvarId : MVarId) : MetaM (Array Expr)