structure Lean.Meta.Try.Collector.InductionCandidate : Type

• fvarId : FVarId
• val : InductiveVal

structure Lean.Meta.Try.Collector.OrdSet (α : Type) [Hashable α] [BEq α] : Type

Set with insertion order preserved.

• elems : Array α
• set : Std.HashSet α

instance Lean.Meta.Try.Collector.instInhabitedOrdSet {a✝ : Type} {a✝¹ : Hashable a✝} {a✝² : BEq a✝} : Inhabited (OrdSet a✝)

def Lean.Meta.Try.Collector.OrdSet.insert {α : Type} {x✝ : Hashable α} {x✝¹ : BEq α} (s : OrdSet α) (a : α) : OrdSet α

def Lean.Meta.Try.Collector.OrdSet.isEmpty {α : Type} {x✝ : Hashable α} {x✝¹ : BEq α} (s : OrdSet α) : Bool

structure Lean.Meta.Try.Collector.Result : Type

• allConsts : OrdSet Name

  All constant symbols occurring in the gal.

• unfoldCandidates : OrdSet Name

  Unfolding candidates.

• eqnCandidates : OrdSet Name

  Equation function candidates.

• funIndCandidates : FunInd.SeenCalls

  Function induction candidates

• indCandidates : Array InductionCandidate

  Induction candidates.

• libSearchResults : OrdSet (Name × Grind.EMatchTheoremKind)

  Relevant declarations by libSearch

structure Lean.Meta.Try.Collector.Context : Type

• config : Try.Config

@[reducible, inline]

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

def Lean.Meta.Try.Collector.getConfig : M Try.Config

def Lean.Meta.Try.Collector.saveConst (declName : Name) : M Unit

def Lean.Meta.Try.Collector.inCurrentModule (declName : Name) : CoreM Bool

Returns true if declName is in the module being compiled.

def Lean.Meta.Try.Collector.isEligible (declName : Name) : M Bool

def Lean.Meta.Try.Collector.saveEqnCandidate (declName : Name) : M Unit

def Lean.Meta.Try.Collector.getEqDefDecl? (declName : Name) : MetaM (Option Name)

def Lean.Meta.Try.Collector.saveUnfoldCandidate (declName : Name) : M Unit

def Lean.Meta.Try.Collector.visitConst (declName : Name) : M Unit

def Lean.Meta.Try.Collector.saveFunInd (e : Expr) (declName : Name) (args : Array Expr) : M Unit

def Lean.Meta.Try.Collector.saveLibSearchCandidates (e : Expr) : M Unit

def Lean.Meta.Try.Collector.visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit

def Lean.Meta.Try.Collector.checkInductive (localDecl : LocalDecl) : M Unit

@[reducible, inline]

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

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

unsafe def Lean.Meta.Try.Collector.main (mvarId : MVarId) (config : Try.Config) : MetaM Result

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

@[reducible, inline]

abbrev Lean.Meta.Try.Info : Type

def Lean.Meta.Try.collect (mvarId : MVarId) (config : Try.Config) : MetaM Info