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 α

Instances For

• Lean.Meta.Try.Collector.instInhabitedOrdSet

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

Equations

• Lean.Meta.Try.Collector.instInhabitedOrdSet = { default := { elems := default, set := default } }

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

Equations

• { elems := elems, set := set }.insert a = if { elems := elems, set := set }.set.contains a = true then { elems := elems, set := set } else { elems := elems.push a, set := set.insert a }

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

Equations

• s.isEmpty = s.elems.isEmpty

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

• allConsts : OrdSet Name

  All constant symbols occurring in the gal.

• unfoldCandidates : OrdSet Name

  Unfolding candiates.

• eqnCandidates : OrdSet Name

  Equation function candiates.

• 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

Equations

• Lean.Meta.Try.Collector.M = ReaderT Lean.Meta.Try.Collector.Context (StateRefT' IO.RealWorld Lean.Meta.Try.Collector.Result Lean.MetaM)

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

Equations

• Lean.Meta.Try.Collector.getConfig = do let __do_lift ← read pure __do_lift.config

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

Equations

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

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

Returns true if declName is in the module being compiled.

Equations

• Lean.Meta.Try.Collector.inCurrentModule declName = do let __do_lift ← Lean.getEnv pure (__do_lift.getModuleIdxFor? declName).isNone

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Try.Collector.visitConst declName = do Lean.Meta.Try.Collector.saveConst declName Lean.Meta.Try.Collector.saveUnfoldCandidate declName

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

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

unsafe def Lean.Meta.Try.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.Try.Collector.main (mvarId : MVarId) (config : Try.Config) : MetaM Result

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Try.Info : Type

Equations

• Lean.Meta.Try.Info = Lean.Meta.Try.Collector.Result

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

Equations

• Lean.Meta.Try.collect mvarId config = Lean.Meta.Try.collect.unsafe_impl_1 mvarId config