- config : Lean.Meta.Simp.Config
- simpTheorems : Lean.Meta.SimpTheoremsArray
- congrTheorems : Lean.Meta.SimpCongrTheorems
- dischargeDepth : Nat
Instances For
Instances For
- cache : Lean.Meta.Simp.Cache
- congrCache : Lean.Meta.Simp.CongrCache
- usedTheorems : Lean.Meta.Simp.UsedSimps
- numSteps : Nat
Instances For
Instances For
Instances For
- post : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step
- discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
Instances For
Instances For
@[inline]
Instances For
@[inline]
def
Lean.Meta.Simp.withSimpTheorems
{α : Type}
(s : Lean.Meta.SimpTheoremsArray)
(x : Lean.Meta.Simp.M α)
: