Documentation

Lean.Meta.Sym.Simp.Result

source
@[reducible, inline]
abbrev Lean.Meta.Sym.Simp.Result.isRfl :
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) (cd₁ : Bool := false) :
      SymM Result

      Chains two simplification steps via Eq.trans. cd₁ is the contextDependent flag from the first step (whose proof is h₁). The output is context-dependent if either step was: in another local context, either step might produce a different result, changing the whole chain.

      Equations
      Instances For
        source
        def Lean.Meta.Sym.Simp.Result.markAsDone :
        Result → Result
        Equations
        Instances For
          source
          def Lean.Meta.Sym.Simp.Result.getResultExpr :
          Expr → Result → Expr
          Equations
          Instances For