source
structure Lean.Meta.Grind.Params :
Type

- config : Grind.Config
- ematch : EMatchTheorems
- inj : InjectiveTheorems
- symPrios : SymbolPriorities
- casesTypes : CasesTypes
- extra : PArray EMatchTheorem
- norm : Simp.Context
- normProcs : Array Simprocs

Instances For

source
def Lean.Meta.Grind.mkParams (config : Grind.Config) :
MetaM Params
Equations

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

Instances For

source
def Lean.Meta.Grind.mkMethods (evalTactic? : Option EvalTactic := none) :
CoreM Methods
Equations

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

Instances For

source
def Lean.Meta.Grind.GrindM.run {α : Type} (x : GrindM α) (params : Params) (evalTactic? : Option EvalTactic := none) :
MetaM α
Equations

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

Instances For

source
structure Lean.Meta.Grind.Result :
Type

- failure? : Option Goal
- issues : List MessageData
- config : Grind.Config
- trace : Trace
- counters : Counters
- simp : Simp.Stats
- splitDiags : PArray SplitDiagInfo

Instances For

source
def Lean.Meta.Grind.Result.hasFailed (r : Result) :
Bool
Equations

- r.hasFailed = r.failure?.isSome

Instances For

source
def Lean.Meta.Grind.Result.toMessageData (result : Result) :
MetaM MessageData
Equations

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

Instances For

source
def Lean.Meta.Grind.mkResult (params : Params) (failure? : Option Goal) :
GrindM Result
Equations

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

Instances For

source
def Lean.Meta.Grind.GrindM.runAtGoal {α : Type} (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) (evalTactic? : Option EvalTactic := none) :
MetaM α
Equations

- Lean.Meta.Grind.GrindM.runAtGoal mvarId params k evalTactic? = (Lean.Meta.withReducible do let goal ← Lean.Meta.Grind.initCore✝ mvarId params k goal).run params evalTactic?

Instances For

source
def Lean.Meta.Grind.main (mvarId : MVarId) (params : Params) :
MetaM Result
Equations

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

Instances For