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