test(tests/lean/reader1): test for perfect roundtripping

This commit is contained in:
Sebastian Ullrich 2018-07-30 14:42:59 -07:00
parent 3127553e72
commit 1c2ca922af

View file

@ -4,6 +4,10 @@ open lean.parser.reader
def show_result (p : lean.parser.reader) (s : string) : io unit :=
let (stx, errors) := p.parse ⟨⟩ s in
when (stx.reprint ≠ s) (
io.print_ln "reprint fail:" *>
io.print_ln stx.reprint
) *>
match errors with
| [] := do
io.print_ln "result: ",