@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Result.isRfl : Result → Bool

def Lean.Meta.Sym.Simp.mkEqTrans (e₁ e₂ h₁ e₃ h₂ : Expr) : SymM Expr

@[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.

def Lean.Meta.Sym.Simp.Result.markAsDone : Result → Result

def Lean.Meta.Sym.Simp.Result.getResultExpr : Expr → Result → Expr