Documentation

Lean.Meta.Sym.Simp.Result

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