Documentation

Lean.Meta.Tactic.Simp.SimpAll

structure Lean.Meta.SimpAll.Entry:

Type

fvarId : Lean.FVarId
userName : Lean.Name
id : Lean.Name
type : Lean.Expr
proof : Lean.Expr

instance Lean.Meta.SimpAll.instInhabitedEntry:

Inhabited Lean.Meta.SimpAll.Entry

Equations

Lean.Meta.SimpAll.instInhabitedEntry = { default := { fvarId := default, userName := default, id := default, type := default, proof := default } }

structure Lean.Meta.SimpAll.State:

Type

@[inline]

abbrev Lean.Meta.SimpAll.M (α : Type) :

Type

Equations

Lean.Meta.SimpAll.M = StateRefT' IO.RealWorld Lean.Meta.SimpAll.State Lean.MetaM

def Lean.Meta.SimpAll.main:

Lean.Meta.SimpAll.M (Option Lean.MVarId)

Equations

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

def Lean.Meta.simpAll (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) :

Lean.MetaM (Option Lean.MVarId)

Equations

Lean.Meta.simpAll mvarId ctx = Lean.Meta.withMVarContext mvarId (StateRefT'.run' Lean.Meta.SimpAll.main { modified := false, mvarId := mvarId, entries := #[], ctx := ctx })