chore: remove builtin subtype notation

src/Lean/Elab/BuiltinNotation.lean

@@ -19,12 +19,6 @@ open Meta
   | `($f $ $a)        => `($f $a)
   | _                 => Macro.throwUnsupported
 
-@[builtinMacro Lean.Parser.Term.subtype] def expandSubtype : Macro := fun stx =>
-  match_syntax stx with
-  | `({ $x : $type // $p }) => `(Subtype (fun ($x:ident : $type) => $p))
-  | `({ $x // $p })         => `(Subtype (fun ($x:ident : _) => $p))
-  | _                       => Macro.throwUnsupported
-
 @[builtinTermElab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
   match_syntax stx with
   | `(⟨$args*⟩) => do

src/Lean/Parser/Term.lean

@@ -73,7 +73,6 @@ def structInstField  := ppGroup $ parser! structInstLVal >> " := " >> termParser
 @[builtinTermParser] def structInst := parser! "{" >> ppHardSpace >> optional («try» (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }"
 def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
-@[builtinTermParser] def subtype := parser! "{ " >> ident >> optType >> " // " >> termParser >> " }"
 @[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec
 @[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole