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, reducible]

abbrev Lean.Meta.Simp.Cache : Type

Equations

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

@[inline, reducible]

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 : Lake.Name) : Bool

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.

@[inline, reducible]

abbrev Lean.Meta.Simp.UsedSimps : Type

Equations

• Lean.Meta.Simp.UsedSimps = Lean.HashMap Lean.Meta.Origin Nat

structure Lean.Meta.Simp.State : Type

• cache : Lean.Meta.Simp.Cache
• congrCache : Lean.Meta.Simp.CongrCache
• usedTheorems : Lean.Meta.Simp.UsedSimps
• numSteps : Nat

@[inline, reducible]

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)

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 x = match x 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

• Lean.Meta.Simp.Step.updateResult x✝ x = match x✝, x with | Lean.Meta.Simp.Step.visit a, r => Lean.Meta.Simp.Step.visit r | Lean.Meta.Simp.Step.done a, r => Lean.Meta.Simp.Step.done r

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, reducible]

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 __do_lift ← read liftM (Lean.Meta.Simp.Methods.pre __do_lift 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 __do_lift ← read liftM (Lean.Meta.Simp.Methods.post __do_lift e)

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

Equations

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

def Lean.Meta.Simp.getConfig : Lean.Meta.SimpM Lean.Meta.Simp.Config

Equations

• Lean.Meta.Simp.getConfig = do let __do_lift ← read pure __do_lift.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 __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.simpTheorems

def Lean.Meta.Simp.getSimpCongrTheorems : Lean.Meta.Simp.M Lean.Meta.SimpCongrTheorems

Equations

• Lean.Meta.Simp.getSimpCongrTheorems = do let __do_lift ← readThe Lean.Meta.Simp.Context pure __do_lift.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.

def Lean.Meta.Simp.recordSimpTheorem (thmId : Lean.Meta.Origin) : Lean.Meta.SimpM Unit

Equations

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

def Lean.Meta.Simp.Result.getProof (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Expr

Equations

• Lean.Meta.Simp.Result.getProof r = match r.proof? with | some p => pure p | none => Lean.Meta.mkEqRefl r.expr

def Lean.Meta.Simp.Result.getProof' (source : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Expr

Similar to Result.getProof, but adds a mkExpectedTypeHint if proof? is none (i.e., result is definitionally equal to input), but we cannot establish that source and r.expr are definitionally when using TransparencyMode.reducible.

Equations

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

def Lean.Meta.Simp.mkCongrFun (r : Lean.Meta.Simp.Result) (a : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.mkCongr (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.mkImpCongr (src : Lean.Expr) (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.removeUnnecessaryCasts (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given the application e, remove unnecessary casts of the form Eq.rec a rfl and Eq.ndrec a rfl.

Equations

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

def Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec (e : Lean.Expr) : Bool

Equations

• Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec e = ((Lean.Expr.isAppOfArity e `Eq.rec 6 || Lean.Expr.isAppOfArity e `Eq.ndrec 6) && Lean.Expr.isAppOf (Lean.Expr.appArg! e) `Eq.refl)

partial def Lean.Meta.Simp.removeUnnecessaryCasts.elimDummyEqRec (e : Lean.Expr) : Lean.Expr

@[specialize #[]]

def Lean.Meta.Simp.congrArgs {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.MonadOptions m] [Lean.MonadTrace m] [Lean.AddMessageContext m] (simp : Lean.Expr → m Lean.Meta.Simp.Result) (dsimp : Lean.Expr → m Lean.Expr) (r : Lean.Meta.Simp.Result) (args : Array Lean.Expr) : m Lean.Meta.Simp.Result

Given a simplified function result r and arguments args, simplify arguments using simp and dsimp. The resulting proof is built using congr and congrFun theorems.

Equations

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

class Lean.Meta.Simp.MonadCongrCache (m : Type → Type) : Type

Helper class for generalizing mkCongrSimp?

• find? : Lean.Expr → m (Option (Option Lean.Meta.CongrTheorem))
• save : Lean.Expr → Option Lean.Meta.CongrTheorem → m Unit

instance Lean.Meta.Simp.instMonadCongrCacheM : Lean.Meta.Simp.MonadCongrCache Lean.Meta.Simp.M

Equations

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

def Lean.Meta.Simp.mkCongrSimp? {m : Type → Type} [Monad m] [MonadLiftT Lean.MetaM m] [Lean.MonadEnv m] [Lean.Meta.Simp.MonadCongrCache m] (f : Lean.Expr) : m (Option Lean.Meta.CongrTheorem)

Retrieve auto-generated congruence lemma for f.

Remark: If all argument kinds are fixed or eq, it returns none because using simple congruence theorems congr, congrArg, and congrFun produces a more compact proof.

Equations

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

@[specialize #[]]

def Lean.Meta.Simp.tryAutoCongrTheorem? {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.Meta.Simp.MonadCongrCache m] [MonadLiftT Lean.MetaM m] [MonadLiftT IO m] [Lean.MonadRef m] [Lean.MonadOptions m] [Lean.MonadTrace m] [Lean.AddMessageContext m] (simp : Lean.Expr → m Lean.Meta.Simp.Result) (dsimp : Lean.Expr → m Lean.Expr) (e : Lean.Expr) : m (Option Lean.Meta.Simp.Result)

Try to use automatically generated congruence theorems. See mkCongrSimp?.

Equations

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

def Lean.Meta.applySimpResultToTarget (mvarId : Lean.MVarId) (target : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.MVarId

Auxiliary method. Given the current target of mvarId, apply r which is a new target and proof that it is equal to the current one.

Equations

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