Documentation

Lean.Meta.Sym.Simp.Result

source
@[reducible, inline]
abbrev Lean.Meta.Sym.Simp.Result.isRfl (result : Result) :
Bool
Instances For
    source
    def Lean.Meta.Sym.Simp.mkEqTrans (e₁ e₂ h₁ e₃ h₂ : Expr) :
    SymM Expr
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Meta.Sym.Simp.mkEqTransResult (e₁ e₂ h₁ : Expr) (r₂ : Result) :
      SymM Result
      Instances For
        source
        def Lean.Meta.Sym.Simp.Result.markAsDone :
        Result → Result
        Instances For
          source
          def Lean.Meta.Sym.Simp.Result.getResultExpr :
          Expr → Result → Expr
          Instances For