Documentation

Lean.Meta.Tactic.Simp.Rewrite

source
def Lean.Meta.Simp.mkEqTrans (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.
source
def Lean.Meta.Simp.synthesizeArgs (thmId : Lean.Meta.Origin) (xs : Array Lean.Expr) (bis : Array Lean.BinderInfo) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) :
Lean.Meta.SimpM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.synthesizeArgs.synthesizeInstance (thmId : Lean.Meta.Origin) (x : Lean.Expr) (type : Lean.Expr) :
Lean.Meta.SimpM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.tryTheoremWithExtraArgs? (e : Lean.Expr) (thm : Lean.Meta.SimpTheorem) (numExtraArgs : Nat) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.tryTheorem? (e : Lean.Expr) (thm : Lean.Meta.SimpTheorem) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite? (e : Lean.Expr) (s : Lean.Meta.SimpTheoremTree) (erased : Lean.PHashSet Lean.Meta.Origin) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (tag : String) (rflOnly : Bool) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewrite?.inErasedSet (erased : Lean.PHashSet Lean.Meta.Origin) (thm : Lean.Meta.SimpTheorem) :
Bool
Equations
source
@[inline]
def Lean.Meta.Simp.andThen (s : Lean.Meta.Simp.Step) (f? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)) :
Lean.Meta.SimpM Lean.Meta.Simp.Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewriteCtorEq? (e : Lean.Expr) :
Lean.MetaM (Option Lean.Meta.Simp.Result)
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Meta.Simp.tryRewriteCtorEq? (e : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewriteUsingDecide? (e : Lean.Expr) :
Lean.MetaM (Option Lean.Meta.Simp.Result)
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Meta.Simp.tryRewriteUsingDecide? (e : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpArith? (e : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpMatchCore? (app : Lean.Meta.MatcherApp) (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.simpMatch? (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (e : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewritePre (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (rflOnly : optParam Bool false) :
Lean.Meta.SimpM Lean.Meta.Simp.Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.rewritePost (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (rflOnly : optParam Bool false) :
Lean.Meta.SimpM Lean.Meta.Simp.Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Simp.preDefault (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) :
Lean.Meta.SimpM Lean.Meta.Simp.Step
Equations
source
def Lean.Meta.Simp.postDefault (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) :
Lean.Meta.SimpM Lean.Meta.Simp.Step
Equations
  • One or more equations did not get rendered due to their size.