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

• fvarId : FVarId
• val : InductiveVal

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

• funIndDeclName : Name
• majors : Array FVarId

instance Lean.Meta.Try.Collector.instHashableFunIndCandidate : Hashable FunIndCandidate

Equations

• Lean.Meta.Try.Collector.instHashableFunIndCandidate = { hash := Lean.Meta.Try.Collector.hashFunIndCandidate✝ }

instance Lean.Meta.Try.Collector.instBEqFunIndCandidate : BEq FunIndCandidate

Equations

• Lean.Meta.Try.Collector.instBEqFunIndCandidate = { beq := Lean.Meta.Try.Collector.beqFunIndCandidate✝ }

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

• allConsts : Std.HashSet Name

  All constant symbols occurring in the gal.

• unfoldCandidates : Std.HashSet Name

  Unfolding candiates.

• eqnCandidates : Std.HashSet Name

  Equation function candiates.

• funIndCandidates : Std.HashSet FunIndCandidate

  Function induction candidates.

• indCandidates : Array InductionCandidate

  Induction candidates.

• libSearchResults : Std.HashSet (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.getFunInductName (declName : Name) : Name

Equations

• Lean.Meta.Try.Collector.getFunInductName declName = declName ++ `induct

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

Equations

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

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.getFunIndMask? (declName indDeclName : Name) : MetaM (Option (Array Bool))

Equations

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

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