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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-14 13:23:25 -07:00
parent 36220b785e
commit 2899e09754
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -326,10 +326,10 @@ f 20
max a b
(Term.app `max [`a `b])
f {x : a} -> b
failed as expected, error: <input>:1:10 unexpected token at this precedence level; consider parenthesizing the term
failed as expected, error: <input>:1:10: unexpected token at this precedence level; consider parenthesizing the term
(x := 20)
failed as expected, error: <input>:1:3 expected ')' or ':'
failed as expected, error: <input>:1:3: expected ')' or ':'
let x 10; x
failed as expected, error: <input>:1:6 expected '|'
failed as expected, error: <input>:1:6: expected '|'
let x := y
failed as expected, error: <input>:1:10 expected term
failed as expected, error: <input>:1:10: expected term