From 34b8e3ef04e2fbed6f4d7efa926a1abda78df2f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Dec 2019 07:35:04 -0800
Subject: [PATCH] feat: elaborate string literals

---
 src/Init/Lean/Elab/Term.lean  | 6 +++---
 tests/lean/run/frontend1.lean | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 36908159c0..f7984777a7 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -918,11 +918,11 @@ fun stx expectedType? => do
 @[builtinTermElab proj] def elabProj : TermElab := elabApp
 @[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabApp
 
-/-
 @[builtinTermElab str] def elabStr : TermElab :=
 fun stx _ => do
-  throw (arbitrary _)
--/
+  match (stx.getArg 0).isStrLit? with
+  | some val => pure $ mkStrLit val
+  | none     => throwError stx.val "ill-formed syntax"
 
 end Term
 
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index c5cb67a85b..9901688b47 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -122,3 +122,4 @@ def m : Monoid Nat :=
 #eval run "#check s.field4.1.length.succ"
 #eval run "#check s.field4.1.map Nat.succ"
 #eval run "#check s.vec[i].1"
+#eval run "#check \"hello\""