diff --git a/Qq/ForLean/ToExpr.lean b/Qq/ForLean/ToExpr.lean
index 80d6868..ccb15f5 100644
--- a/Qq/ForLean/ToExpr.lean
+++ b/Qq/ForLean/ToExpr.lean
@@ -2,12 +2,6 @@ import Lean
 
 open Lean
 
-instance : ToExpr Int where
-  toTypeExpr := .const ``Int []
-  toExpr i := match i with
-    | .ofNat n => mkApp (.const ``Int.ofNat []) (toExpr n)
-    | .negSucc n => mkApp (.const ``Int.negSucc []) (toExpr n)
-
 instance : ToExpr MVarId where
   toTypeExpr := .const ``MVarId []
   toExpr i := mkApp (.const ``MVarId.mk []) (toExpr i.name)
diff --git a/Qq/Typ.lean b/Qq/Typ.lean
index 71cf37c..96eb048 100644
--- a/Qq/Typ.lean
+++ b/Qq/Typ.lean
@@ -37,7 +37,7 @@ protected abbrev Quoted.ty (t : Quoted α) : Expr := α
 
 You should usually write this using the notation `$lhs =Q $rhs`.
 -/
-structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α) : Prop :=
+structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α) : Prop where
   unsafeIntro ::
 
 /--
@@ -45,7 +45,7 @@ structure QuotedDefEq {α : Quoted (.sort u)} (lhs rhs : Quoted α) : Prop :=
 
 You should usually write this using the notation `$u =QL $v`.
 -/
-structure QuotedLevelDefEq (u v : Level) : Prop :=
+structure QuotedLevelDefEq (u v : Level) : Prop where
   unsafeIntro ::
 
 open Meta in