structure Lean.Meta.Grind.Preprocessor.Context : Type

• simp : Lean.Meta.Simp.Context
• simprocs : Array Lean.Meta.Simprocs

instance Lean.Meta.Grind.Preprocessor.instInhabitedContext : Inhabited Lean.Meta.Grind.Preprocessor.Context

Equations

• Lean.Meta.Grind.Preprocessor.instInhabitedContext = { default := { simp := default, simprocs := default } }

structure Lean.Meta.Grind.Preprocessor.State : Type

• simpStats : Lean.Meta.Simp.Stats
• goals : Lean.PArray Lean.Meta.Grind.Goal

instance Lean.Meta.Grind.Preprocessor.instInhabitedState : Inhabited Lean.Meta.Grind.Preprocessor.State

Equations

• Lean.Meta.Grind.Preprocessor.instInhabitedState = { default := { simpStats := default, goals := default } }

@[reducible, inline]

abbrev Lean.Meta.Grind.Preprocessor.PreM (α : Type) : Type

Equations

• Lean.Meta.Grind.Preprocessor.PreM = ReaderT Lean.Meta.Grind.Preprocessor.Context (StateRefT' IO.RealWorld Lean.Meta.Grind.Preprocessor.State Lean.Meta.Grind.GrindM)

def Lean.Meta.Grind.Preprocessor.PreM.run {α : Type} (x : Lean.Meta.Grind.Preprocessor.PreM α) : Lean.Meta.Grind.GrindM α

Equations

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

def Lean.Meta.Grind.Preprocessor.simp (_goal : Lean.Meta.Grind.Goal) (e : Lean.Expr) : Lean.Meta.Grind.Preprocessor.PreM Lean.Meta.Simp.Result

Equations

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

inductive Lean.Meta.Grind.Preprocessor.IntroResult : Type

• done : Lean.Meta.Grind.Preprocessor.IntroResult
• newHyp (fvarId : Lean.FVarId) (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.Preprocessor.IntroResult
• newDepHyp (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.Preprocessor.IntroResult
• newLocal (fvarId : Lean.FVarId) (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.Preprocessor.IntroResult

def Lean.Meta.Grind.Preprocessor.introNext (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.Preprocessor.PreM Lean.Meta.Grind.Preprocessor.IntroResult

Equations

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

def Lean.Meta.Grind.Preprocessor.pushResult (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.Preprocessor.PreM Unit

Equations

• Lean.Meta.Grind.Preprocessor.pushResult goal = modify fun (s : Lean.Meta.Grind.Preprocessor.State) => { simpStats := s.simpStats, goals := Lean.PersistentArray.push s.goals goal }

def Lean.Meta.Grind.Preprocessor.isCasesCandidate (fvarId : Lean.FVarId) : Lean.MetaM Bool

Equations

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

def Lean.Meta.Grind.Preprocessor.applyCases? (goal : Lean.Meta.Grind.Goal) (fvarId : Lean.FVarId) : Lean.MetaM (Option (List Lean.Meta.Grind.Goal))

Equations

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

def Lean.Meta.Grind.Preprocessor.applyInjection? (goal : Lean.Meta.Grind.Goal) (fvarId : Lean.FVarId) : Lean.MetaM (Option Lean.Meta.Grind.Goal)

Equations

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

partial def Lean.Meta.Grind.Preprocessor.loop (goal : Lean.Meta.Grind.Goal) : Lean.Meta.Grind.Preprocessor.PreM Unit

def Lean.Meta.Grind.Preprocessor.preprocess (mvarId : Lean.MVarId) : Lean.Meta.Grind.Preprocessor.PreM Lean.Meta.Grind.Preprocessor.State

Equations

• Lean.Meta.Grind.Preprocessor.preprocess mvarId = do let __do_lift ← liftM (Lean.Meta.Grind.mkGoal mvarId) Lean.Meta.Grind.Preprocessor.loop __do_lift get

def Lean.Meta.Grind.main (mvarId : Lean.MVarId) (mainDeclName : Lean.Name) : Lean.MetaM (List Lean.MVarId)

Equations

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