Lean.Meta.Tactic.Simp.Types

Lean.Meta.Simp.instInhabitedContext = { default := { config := default, simpLemmas := default, congrLemmas := default, parent? := default, dischargeDepth := default } }

source

def Lean.Meta.Simp.Context.mkDefault :

Lean.MetaM Lean.Meta.Simp.Context

Equations

Lean.Meta.Simp.Context.mkDefault = do let a ← liftM Lean.Meta.getSimpLemmas let a_1 ← Lean.Meta.getCongrLemmas pure { config := { maxSteps := Lean.Meta.Simp.defaultMaxSteps, maxDischargeDepth := 2, contextual := false, memoize := true, singlePass := false, zeta := true, beta := true, eta := true, etaStruct := true, iota := true, proj := true, decide := true }, simpLemmas := a, congrLemmas := a_1, parent? := none, dischargeDepth := 0 }

source

structure Lean.Meta.Simp.State :

Type

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

source

@[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)

source

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) }

source

inductive Lean.Meta.Simp.Step :

Type

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

source

instance Lean.Meta.Simp.instInhabitedStep :

Inhabited Lean.Meta.Simp.Step

Equations

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

source

def Lean.Meta.Simp.Step.result :

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

Equations

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

source

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)

source

instance Lean.Meta.Simp.instInhabitedMethods :

Inhabited Lean.Meta.Simp.Methods

Equations

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

source

@[inline]

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

Type

Equations

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

source

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)

source

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)

source

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)

source

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

source

@[inline]

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

Lean.Meta.Simp.M α

Equations

Lean.Meta.Simp.withParent parent f = withTheReader Lean.Meta.Simp.Context (fun ctx => { config := ctx.config, simpLemmas := ctx.simpLemmas, congrLemmas := ctx.congrLemmas, parent? := some parent, dischargeDepth := ctx.dischargeDepth }) f

source

def Lean.Meta.Simp.getSimpLemmas :

Lean.Meta.Simp.M Lean.Meta.SimpLemmas

Equations

Lean.Meta.Simp.getSimpLemmas = do let a ← readThe Lean.Meta.Simp.Context pure a.simpLemmas

source

def Lean.Meta.Simp.getCongrLemmas :

Lean.Meta.Simp.M Lean.Meta.CongrLemmas

Equations

Lean.Meta.Simp.getCongrLemmas = do let a ← readThe Lean.Meta.Simp.Context pure a.congrLemmas

source

@[inline]

def Lean.Meta.Simp.withSimpLemmas {α : Type} (s : Lean.Meta.SimpLemmas) (x : Lean.Meta.Simp.M α) :

Lean.Meta.Simp.M α

Equations

Lean.Meta.Simp.withSimpLemmas s x = do let a ← get let cacheSaved : Lean.Meta.Simp.Cache := a.cache modify fun s => { cache := ∅, numSteps := s.numSteps } tryFinally (withTheReader Lean.Meta.Simp.Context (fun ctx => { config := ctx.config, simpLemmas := s, congrLemmas := ctx.congrLemmas, parent? := ctx.parent?, dischargeDepth := ctx.dischargeDepth }) x) (modify fun s => { cache := cacheSaved, numSteps := s.numSteps })