Merge remote-tracking branch 'origin/master' into lean-pr-testing-5323

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)

Qq/Typ.lean

@@ -37,15 +37,15 @@ 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 ::
 
 /--
 `QuotedLevelDefEq u v` says that the levels `u` and `v` are definitionally equal.
 
 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