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.
84 lines
No EOL
2.4 KiB
Text
84 lines
No EOL
2.4 KiB
Text
Success! Final stack:
|
|
(Lean.Doc.Syntax.ul
|
|
"ul{"
|
|
[(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.code
|
|
"`"
|
|
(str "\"structure\"")
|
|
"`")
|
|
(Lean.Doc.Syntax.text (str "\" and \""))
|
|
(Lean.Doc.Syntax.code
|
|
"`"
|
|
(str "\"inductive\"")
|
|
"`")
|
|
(Lean.Doc.Syntax.text
|
|
(str "\" commands\""))]
|
|
"}")
|
|
(Lean.Doc.Syntax.ul
|
|
"ul{"
|
|
[(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.link
|
|
"["
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"#5842\""))]
|
|
"]"
|
|
(Lean.Doc.Syntax.url
|
|
"("
|
|
(str
|
|
"\"https://github.com/leanprover/lean4/pull/5842\"")
|
|
")"))
|
|
(Lean.Doc.Syntax.text
|
|
(str "\" and \""))
|
|
(Lean.Doc.Syntax.link
|
|
"["
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"#5783\""))]
|
|
"]"
|
|
(Lean.Doc.Syntax.url
|
|
"("
|
|
(str
|
|
"\"https://github.com/leanprover/lean4/pull/5783\"")
|
|
")"))
|
|
(Lean.Doc.Syntax.text
|
|
(str
|
|
"\" implement a feature where the \""))
|
|
(Lean.Doc.Syntax.code
|
|
"`"
|
|
(str "\"structure\"")
|
|
"`")
|
|
(Lean.Doc.Syntax.text
|
|
(str
|
|
"\" command can now define recursive inductive types:\""))]
|
|
"}")
|
|
(Lean.Doc.Syntax.codeblock
|
|
"```"
|
|
[`lean []]
|
|
"\n"
|
|
(str
|
|
"\"structure Tree where\\n n : Nat\\n children : Fin n → Tree\\n\\ndef Tree.size : Tree → Nat\\n | {n, children} => Id.run do\\n let mut s := 0\\n for h : i in [0 : n] do\\n s := s + (children ⟨i, h.2⟩).size\\n pure s\\n\"")
|
|
"```")])
|
|
(Lean.Doc.Syntax.li
|
|
"*"
|
|
[(Lean.Doc.Syntax.para
|
|
"para{"
|
|
[(Lean.Doc.Syntax.link
|
|
"["
|
|
[(Lean.Doc.Syntax.text
|
|
(str "\"#5814\""))]
|
|
"]"
|
|
(Lean.Doc.Syntax.url
|
|
"("
|
|
(str
|
|
"\"https://github.com/leanprover/lean4/pull/5814\"")
|
|
")"))
|
|
(Lean.Doc.Syntax.text (str "\" \""))]
|
|
"}")])]
|
|
"}")])]
|
|
"}")
|
|
All input consumed. |