From 0ddc2e5efb51281d072a3e01bc0bff4da648949b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 14 Nov 2020 08:42:03 -0800
Subject: [PATCH] chore: remove builtin subtype notation

---
 src/Lean/Elab/BuiltinNotation.lean | 6 ------
 src/Lean/Parser/Term.lean          | 1 -
 2 files changed, 7 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 205a9a29ef..ba814f021a 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/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
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index d3ea503e5a..93607dc7cd 100644
--- a/src/Lean/Parser/Term.lean
+++ b/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