Success! Final stack:
  (Lean.Doc.Syntax.footnote
   "[^"
   (str "\"1\"")
   "]")
All input consumed.