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

chore: fix test

Browse source 
@Kha the tests `Reparen.lean` and `Reformat.lean` are still
broken. Could you please take a look?
They broke because I changed the `match` syntax at 3ce794c58.
This commit is contained in:
Leonardo de Moura 2020-08-10 10:20:57 -07:00
parent 9bd4acd9c9
commit e59735bde9
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/compiler/termparsertest1.lean.expected.out
View file

@ -230,7 +230,7 @@ match x with
| none => false
(Term.match
"match"
[(Term.id `x [])]
[[] (Term.id `x [])]
[]
"with"
["|"]
@ -246,7 +246,7 @@ match x with
(Term.match
"match"
[(Term.id `x [])]
[[] (Term.id `x [])]
[]
"with"
["|"]
@ -255,7 +255,7 @@ match x with
"=>"
(Term.match
"match"
[(Term.id `y [])]
[[] (Term.id `y [])]
[]
"with"
["|"]