@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Result.isRfl (result : Result) : Bool

Equations

• Lean.Meta.Sym.Simp.Result.rfl.isRfl = true
• result.isRfl = false

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

Equations

• Lean.Meta.Sym.Simp.mkEqTrans e₁ e₂ h₁ e₃ h₂ = do let α ← Lean.Meta.Sym.inferType e₁ let u ← Lean.Meta.Sym.getLevel α pure (Lean.mkApp6 (Lean.mkConst `Eq.trans [u]) α e₁ e₂ e₃ h₁ h₂)

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.mkEqTransResult (e₁ e₂ h₁ : Expr) (r₂ : Result) : SymM Result

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Sym.Simp.mkEqTransResult e₁ e₂ h₁ (Lean.Meta.Sym.Simp.Result.rfl done) = pure (Lean.Meta.Sym.Simp.Result.step e₂ h₁ done)

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

Equations

• (Lean.Meta.Sym.Simp.Result.rfl done).markAsDone = Lean.Meta.Sym.Simp.Result.rfl true
• (Lean.Meta.Sym.Simp.Result.step e₃ h₂ done).markAsDone = Lean.Meta.Sym.Simp.Result.step e₃ h₂ true