feat: elaborate string literals

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
 

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\""