feat: elaborate subtype

src/Init/Lean/Elab/BuiltinNotation.lean

@@ -26,6 +26,12 @@ adaptExpander $ fun stx => match_syntax stx with
 | `(if $cond then $t else $e)      => `(ite $cond $t $e)
 | _                                => unreachable!
 
+@[builtinTermElab subtype] def elabSubtype : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `({ $x : $type // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : $type) => $p))
+| `({ $x // $p })         => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : _) => $p))
+| _                       => unreachable!
+
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do
   -- term `op` term

tests/lean/run/frontend1.lean

@@ -180,3 +180,5 @@ f a
 #eval run "#check fun (a : Array Nat) => a.size"
 #eval run "#check if 0 = 1 then 'a' else 'b'"
 #eval run "#check fun (i : Nat) (a : Array Nat) => if h : i < a.size then a.get (Fin.mk i h) else i"
+#eval run "#check { x : Nat // x > 0 }"
+#eval run "#check { x // x > 0 }"