From 0ffd1526bd9507401d0725166e363aa571319fff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Jan 2020 10:12:19 -0800
Subject: [PATCH] feat: elaborate subtype

---
 src/Init/Lean/Elab/BuiltinNotation.lean | 6 ++++++
 tests/lean/run/frontend1.lean           | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index 835c052d62..36e9c23026 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/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
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 2b06cfc3e3..38169ef6d0 100644
--- a/tests/lean/run/frontend1.lean
+++ b/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 }"