From c08fcdb6626b528c67ef9e349e86939fd34b3cd9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Jan 2020 14:21:49 -0500
Subject: [PATCH] chore: ad-hoc `match_syntax` support in the new frontend

---
 src/Init/Lean/Elab/Quotation.lean   | 2 +-
 src/Init/Lean/Elab/TermBinders.lean | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 63bca64687..6824b4f0d4 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -275,7 +275,7 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt 
   cond ← match info.argPats with
   | some pats => `(Syntax.isOfKind discr $(quote kind) && Array.size (Syntax.getArgs discr) == $(quote pats.size))
   | none      => `(Syntax.isOfKind discr $(quote kind));
-  `(let discr := $discr; if $cond then $yes else $no)
+  `(let discr := $discr; if coe $cond then $yes else $no)
 | _, _ => unreachable!
 
 private partial def getPatternVarsAux : Syntax → TermElabM (List Syntax)
diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/TermBinders.lean
index ebb38fd52f..a372590a2c 100644
--- a/src/Init/Lean/Elab/TermBinders.lean
+++ b/src/Init/Lean/Elab/TermBinders.lean
@@ -302,7 +302,13 @@ def elabLetPatDecl (ref : Syntax) (decl body : Syntax) (expectedType? : Option E
 throwError decl "not implemented yet"
 
 @[builtinTermElab «let»] def elabLet : TermElab :=
-fun stx expectedType? => do
+fun stx expectedType? => match_syntax stx with
+| `(let $id:id := $decl; $body) => do
+  -- HACK: support single-id pattern let (as produced by quotations) by translation to ident let for now
+  let id := id.getArg 0;
+  stx ← `(let $id:ident := $decl; $body);
+  elabTerm stx expectedType?
+| _ => do
   -- `let` decl `;` body
   let ref      := stx;
   let decl     := stx.getArg 1;