Success! Final stack:
  (Lean.Doc.Syntax.code
   "``"
   (str "\"foo bar\"")
   "``")
All input consumed.