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