Instances For
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))
:
Instances For
def
Lean.Meta.Simp.synthesizeArgs.synthesizeInstance
(thmId : Lean.Meta.Origin)
(x : Lean.Expr)
(type : Lean.Expr)
:
Instances For
def
Lean.Meta.Simp.tryTheoremWithExtraArgs?
(e : Lean.Expr)
(thm : Lean.Meta.SimpTheorem)
(numExtraArgs : Nat)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Instances For
def
Lean.Meta.Simp.tryTheorem?
(e : Lean.Expr)
(thm : Lean.Meta.SimpTheorem)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Instances For
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)
:
Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
Instances For
def
Lean.Meta.Simp.rewrite?.inErasedSet
(erased : Lean.PHashSet Lean.Meta.Origin)
(thm : Lean.Meta.SimpTheorem)
:
Instances For
@[inline]
def
Lean.Meta.Simp.andThen
(s : Lean.Meta.Simp.Step)
(f? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Step))
:
Instances For
Instances For
@[inline]
Instances For
Instances For
Instances For
def
Lean.Meta.Simp.simpMatchCore?
(app : Lean.Meta.MatcherApp)
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Instances For
def
Lean.Meta.Simp.simpMatch?
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
(e : Lean.Expr)
:
Instances For
def
Lean.Meta.Simp.rewritePre
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
(rflOnly : optParam Bool false)
:
Instances For
def
Lean.Meta.Simp.rewritePost
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
(rflOnly : optParam Bool false)
:
Instances For
def
Lean.Meta.Simp.preDefault
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
:
Instances For
def
Lean.Meta.Simp.postDefault
(e : Lean.Expr)
(discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))
: