Documentation

Lean.Meta.Tactic.Simp.Types

structure Lean.Meta.Simp.Result:

Type

expr : Lean.Expr
proof? : Option Lean.Expr
dischargeDepth : Nat

instance Lean.Meta.Simp.instInhabitedResult:

Inhabited Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.instInhabitedResult = { default := { expr := default, proof? := default, dischargeDepth := default } }

@[inline]

abbrev Lean.Meta.Simp.Cache:

Type

Equations

Lean.Meta.Simp.Cache = Lean.ExprMap Lean.Meta.Simp.Result

@[inline]

abbrev Lean.Meta.Simp.CongrCache:

Type

Equations

Lean.Meta.Simp.CongrCache = Lean.ExprMap (Option Lean.Meta.CongrTheorem)

structure Lean.Meta.Simp.Context:

Type

config : Lean.Meta.Simp.Config
simpTheorems : Lean.Meta.SimpTheoremsArray
congrTheorems : Lean.Meta.SimpCongrTheorems
parent? : Option Lean.Expr
dischargeDepth : Nat

instance Lean.Meta.Simp.instInhabitedContext:

Inhabited Lean.Meta.Simp.Context

Equations

Lean.Meta.Simp.instInhabitedContext = { default := { config := default, simpTheorems := default, congrTheorems := default, parent? := default, dischargeDepth := default } }

def Lean.Meta.Simp.Context.isDeclToUnfold (ctx : Lean.Meta.Simp.Context) (declName : Lean.Name) :

Equations

Lean.Meta.Simp.Context.isDeclToUnfold ctx declName = Lean.Meta.SimpTheoremsArray.isDeclToUnfold ctx.simpTheorems declName

def Lean.Meta.Simp.Context.mkDefault:

Lean.MetaM Lean.Meta.Simp.Context

Equations

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

structure Lean.Meta.Simp.State:

Type

cache : Lean.Meta.Simp.Cache
congrCache : Lean.Meta.Simp.CongrCache
numSteps : Nat

@[inline]

abbrev Lean.Meta.Simp.SimpM (α : Type) :

Type

Equations

Lean.Meta.SimpM = ReaderT Lean.Meta.Simp.Context (StateRefT' IO.RealWorld Lean.Meta.Simp.State Lean.MetaM)

instance Lean.Meta.Simp.instMonadBacktrackSavedStateSimpM:

Lean.MonadBacktrack Lean.Meta.SavedState Lean.Meta.SimpM

Equations

Lean.Meta.Simp.instMonadBacktrackSavedStateSimpM = { saveState := liftM Lean.Meta.saveState, restoreState := fun s => liftM (Lean.Meta.SavedState.restore s) }

inductive Lean.Meta.Simp.Step:

Type

visit: Lean.Meta.Simp.Result → Lean.Meta.Simp.Step
done: Lean.Meta.Simp.Result → Lean.Meta.Simp.Step

instance Lean.Meta.Simp.instInhabitedStep:

Inhabited Lean.Meta.Simp.Step

Equations

Lean.Meta.Simp.instInhabitedStep = { default := Lean.Meta.Simp.Step.visit default }

def Lean.Meta.Simp.Step.result:

Lean.Meta.Simp.Step → Lean.Meta.Simp.Result

Equations

Lean.Meta.Simp.Step.result _fun_discr = match _fun_discr with | Lean.Meta.Simp.Step.visit r => r | Lean.Meta.Simp.Step.done r => r

def Lean.Meta.Simp.Step.updateResult:

Lean.Meta.Simp.Step → Lean.Meta.Simp.Result → Lean.Meta.Simp.Step

Equations

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

structure Lean.Meta.Simp.Methods:

Type

pre : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
post : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)

instance Lean.Meta.Simp.instInhabitedMethods:

Inhabited Lean.Meta.Simp.Methods

Equations

Lean.Meta.Simp.instInhabitedMethods = { default := { pre := default, post := default, discharge? := default } }

@[inline]

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

Type

Equations

Lean.Meta.Simp.M = ReaderT Lean.Meta.Simp.Methods Lean.Meta.SimpM

def Lean.Meta.Simp.pre (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Step

Equations

Lean.Meta.Simp.pre e = do let a ← read liftM (Lean.Meta.Simp.Methods.pre a e)

def Lean.Meta.Simp.post (e : Lean.Expr) :

Lean.Meta.Simp.M Lean.Meta.Simp.Step

Equations

Lean.Meta.Simp.post e = do let a ← read liftM (Lean.Meta.Simp.Methods.post a e)

def Lean.Meta.Simp.discharge? (e : Lean.Expr) :

Lean.Meta.Simp.M (Option Lean.Expr)

Equations

Lean.Meta.Simp.discharge? e = do let a ← read liftM (Lean.Meta.Simp.Methods.discharge? a e)

def Lean.Meta.Simp.getConfig:

Lean.Meta.Simp.M Lean.Meta.Simp.Config

Equations

Lean.Meta.Simp.getConfig = do let a ← readThe Lean.Meta.Simp.Context pure a.config

@[inline]

def Lean.Meta.Simp.withParent {α : Type} (parent : Lean.Expr) (f : Lean.Meta.Simp.M α) :

Lean.Meta.Simp.M α

Equations

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

def Lean.Meta.Simp.getSimpTheorems:

Lean.Meta.Simp.M Lean.Meta.SimpTheoremsArray

Equations

Lean.Meta.Simp.getSimpTheorems = do let a ← readThe Lean.Meta.Simp.Context pure a.simpTheorems

def Lean.Meta.Simp.getSimpCongrTheorems:

Lean.Meta.Simp.M Lean.Meta.SimpCongrTheorems

Equations

Lean.Meta.Simp.getSimpCongrTheorems = do let a ← readThe Lean.Meta.Simp.Context pure a.congrTheorems

@[inline]

def Lean.Meta.Simp.withSimpTheorems {α : Type} (s : Lean.Meta.SimpTheoremsArray) (x : Lean.Meta.Simp.M α) :

Lean.Meta.Simp.M α

Equations

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