michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean): test output

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-13 09:57:58 -07:00
parent 7c047def97
commit b3c89070e3
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
tests/lean/bad_quoted_symbol.lean.expected.out
View file

@ -1,5 +1,5 @@
tests/lean/bad_quoted_symbol.lean:2:12: error: first character of a quoted symbols cannot be a digit bad_quoted_symbol.lean:2:12: error: first character of a quoted symbols cannot be a digit
tests/lean/bad_quoted_symbol.lean:3:16: error: unexpected space inside of quoted symbol bad_quoted_symbol.lean:3:16: error: unexpected space inside of quoted symbol
tests/lean/bad_quoted_symbol.lean:4:14: error: unexpected end of quoted symbol bad_quoted_symbol.lean:4:14: error: unexpected end of quoted symbol
tests/lean/bad_quoted_symbol.lean:5:10: error: invalid quoted symbol, invalid character bad_quoted_symbol.lean:5:10: error: invalid quoted symbol, invalid character
tests/lean/bad_quoted_symbol.lean:5:10: error: invalid notation declaration, symbol expected bad_quoted_symbol.lean:5:10: error: invalid notation declaration, symbol expected