diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean index 0f56dc29d4..a596974b2f 100644 --- a/src/Lean/ToExpr.lean +++ b/src/Lean/ToExpr.lean @@ -14,10 +14,6 @@ class ToExpr (α : Type u) where export ToExpr (toExpr toTypeExpr) -instance : ToExpr Expr where - toExpr := id - toTypeExpr := mkConst ``Expr - instance : ToExpr Nat where toExpr := mkNatLit toTypeExpr := mkConst ``Nat