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

Instances For

• Lean.Meta.FunInd.instBEqCall
• Lean.Meta.FunInd.instHashableCall

instance Lean.Meta.FunInd.instHashableCall : Hashable Call

Equations

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

instance Lean.Meta.FunInd.instBEqCall : BEq Call

Equations

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

structure Lean.Meta.FunInd.SeenCalls : Type

• calls : Array Expr

  the full calls

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

  only function name and relevant arguments

Instances For

• Lean.Meta.FunInd.instEmptyCollectionSeenCalls

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.

unsafe def Lean.Meta.FunInd.Collector.main.go (mvarId : MVarId) : StateRefT' IO.RealWorld Cache M Unit

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