From 1512ccfdc83df5e0336ef6f25afd7e56d0445995 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Jan 2020 20:11:42 -0800
Subject: [PATCH] chore: reacticate `where` elaboration

---
 src/Init/Lean/Elab/BuiltinNotation.lean | 12 +++++-------
 tests/lean/run/macroid.lean             |  2 ++
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index 7f2a86379f..584fdb9540 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -77,18 +77,16 @@ adaptExpander $ fun stx => match_syntax stx with
 | `(have $x : $type := $val; $body)   => `((fun ($x:ident : $type) => $body) $val)
 | _                                   => throwUnsupportedSyntax
 
-/-
-@[termElab «where»] def elabWhere : TermElab :=
+@[builtinTermElab «where»] def elabWhere : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `($body where $decls*) =>  do
+| `($body where $decls:letDecl*) =>  do
   let decls := decls.getEvenElems;
   decls.foldrM
-    (fun decl body => `(let $decl; $body))
+    (fun decl body => `(let $decl:letDecl; $body))
     body
 | _                      => throwUnsupportedSyntax
--/
 
-@[termElab «parser!»] def elabParserMacro : TermElab :=
+@[builtinTermElab «parser!»] def elabParserMacro : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `(parser! $e) => do
   some declName ← getDeclName?
@@ -107,7 +105,7 @@ adaptExpander $ fun stx => match_syntax stx with
   | _             => throwError stx "invalid `parser!` macro, unexpected declaration name"
 | _             => throwUnsupportedSyntax
 
-@[termElab «tparser!»] def elabTParserMacro : TermElab :=
+@[builtinTermElab «tparser!»] def elabTParserMacro : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
 | `(tparser! $e) => do
   declName? ← getDeclName?;
diff --git a/tests/lean/run/macroid.lean b/tests/lean/run/macroid.lean
index 3c91c58e2a..46f670fbeb 100644
--- a/tests/lean/run/macroid.lean
+++ b/tests/lean/run/macroid.lean
@@ -23,3 +23,5 @@ macro_rules
 | `(test $x:id) => `(let $x := 0; $x)
 
 #check fun (x : Nat) => test x
+
+#check x where y := 1; where x := y + 1