max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/lean/parser1): fix reprinting (`eoi node was missing)

Browse source
This commit is contained in:
Sebastian Ullrich 2018-10-15 12:47:32 +02:00
parent a820b9955f
commit db6b9db07e
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/parser1.lean
View file

@ -115,7 +115,7 @@ def run_frontend (input : string) : except_t string io unit := do
when ¬(cmd'.is_of_kind module.eoi) $
io.println "elaborator died!!",
msgs.to_list.mfor $ λ e, io.println e.text,
pure (sum.inr outs.reverse)
pure $ sum.inr (out::outs).reverse
}
| coroutine_result_core.yielded elab_out elab_k := do {
elab_out.messages.to_list.mfor $ λ e, io.println e.text,
@ -126,7 +126,7 @@ def run_frontend (input : string) : except_t string io unit := do
},
check_reprint outs input/-,
let stx := syntax.node ⟨none, outs.map (λ r, r.cmd)⟩,
let stx := stx.update_leading s,
let stx := stx.update_leading input,
io.println "result:",
io.println (to_string stx)-/
#exit