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

Equations

• Lean.Meta.FunInd.instHashableCall.hash { expr := a, relevantArgs := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[implicit_reducible]

instance Lean.Meta.FunInd.instHashableCall : Hashable Call

Equations

• Lean.Meta.FunInd.instHashableCall = { hash := Lean.Meta.FunInd.instHashableCall.hash }

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

Equations

• Lean.Meta.FunInd.instBEqCall.beq { expr := a, relevantArgs := a_1 } { expr := b, relevantArgs := b_1 } = (a == b && a_1 == b_1)
• Lean.Meta.FunInd.instBEqCall.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Lean.Meta.FunInd.instBEqCall : BEq Call

Equations

• Lean.Meta.FunInd.instBEqCall = { beq := Lean.Meta.FunInd.instBEqCall.beq }

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

Equations

• Lean.Meta.FunInd.instEmptyCollectionSeenCalls = { emptyCollection := { calls := #[], seen := ∅ } }

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

Equations

• sc.isEmpty = sc.calls.isEmpty

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

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

Equations

• Lean.Meta.FunInd.Collector.M = ReaderT Lean.Meta.FunIndInfo (StateRefT' IO.RealWorld Lean.Meta.FunInd.SeenCalls Lean.MetaM)

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

Equations

• Lean.Meta.FunInd.Collector.saveFunInd e funIndInfo args = do let __do_lift ← get let __do_lift ← liftM (Lean.Meta.FunInd.SeenCalls.push e funIndInfo args __do_lift) set __do_lift

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

Equations

• Lean.Meta.FunInd.Collector.visitApp e funIndInfo args = Lean.Meta.FunInd.Collector.saveFunInd e funIndInfo args

@[reducible, inline]

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

Equations

• Lean.Meta.FunInd.Collector.Cache = Lean.PtrSet Lean.Expr

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.FunInd.collect needle mvarId = Lean.Meta.FunInd.collect.unsafe_impl_3✝ needle mvarId