From 16aff9a182e357c3e23ff6c90663fb8ecbca0054 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Jan 2020 14:16:20 -0800
Subject: [PATCH] feat: elaborate `have`

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

diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index ae2cce250b..dd714a7c00 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -60,6 +60,14 @@ adaptExpander $ fun stx => match_syntax stx with
 | `(show $type from $val) => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $thisId) $val)
 | _                       => throwUnexpectedSyntax stx "show-from"
 
+@[builtinTermElab «have»] def elabHave : TermElab :=
+adaptExpander $ fun stx => match_syntax stx with
+| `(have $type from $val; $body)      => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
+| `(have $type := $val; $body)        => let thisId := mkTermId stx `this; `((fun ($thisId : $type) => $body) $val)
+| `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
+| `(have $x : $type := $val; $body)   => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
+| _                                   => throwUnexpectedSyntax stx "have"
+
 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 baa6b27617..95ec912c52 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -187,3 +187,7 @@ f a
 #eval run "#check let x := ⟨1, 2⟩; Prod.fst x"
 #eval run "#check show Nat from 1"
 #eval run "#check show Int from 1"
+#eval run "#check have Nat from one + zero; this + this"
+#eval run "#check have x : Nat from one + zero; x + x"
+#eval run "#check have Nat := one + zero; this + this"
+#eval run "#check have x : Nat := one + zero; x + x"