a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
47 lines
No EOL
1.1 KiB
Text
47 lines
No EOL
1.1 KiB
Text
Success! Final stack:
|
|
[(Lean.Doc.Syntax.ul
|
|
"ul{"
|
|
[(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.ul
|
|
"ul{"
|
|
[(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"A1\""))]
|
|
"}")])
|
|
(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"A2\""))]
|
|
"}")])]
|
|
"}")])
|
|
(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.text (str "\"B\""))]
|
|
"}")
|
|
(Lean.Doc.Syntax.ul
|
|
"ul{"
|
|
[(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"B1\""))]
|
|
"}")])
|
|
(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"B2\""))]
|
|
"}")])]
|
|
"}")])]
|
|
"}")]
|
|
All input consumed. |