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

Equations

• (Lean.Meta.Sym.DSimp.Result.rfl done).markAsDone = Lean.Meta.Sym.DSimp.Result.rfl true
• (Lean.Meta.Sym.DSimp.Result.step e done).markAsDone = Lean.Meta.Sym.DSimp.Result.step e true

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

Equations

• Lean.Meta.Sym.DSimp.Result.getResultExpr x✝ (Lean.Meta.Sym.DSimp.Result.rfl done) = x✝
• Lean.Meta.Sym.DSimp.Result.getResultExpr x✝ (Lean.Meta.Sym.DSimp.Result.step e done) = e