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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-31 14:58:15 -07:00
parent c35f96ac82
commit 92193e7d70
5 changed files with 28 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
tests/lean/348.lean.expected.out
View file

@ -1 +1,9 @@
348.lean:3:24: error: expected ')'
348.lean:2:2-2:47: error: application type mismatch
pure PUnit.unit
argument
PUnit.unit
has type
PUnit : Sort ?u
but is expected to have type
String : Type

3
tests/lean/exitAfterParseError.lean.expected.out
View file

@ -1 +1,2 @@
exitAfterParseError.lean:5:0: error: expected ':=', 'where' or '|'
exitAfterParseError.lean:5:0: error: unexpected declaration body; expected ':=', 'where' or '|'
exitAfterParseError.lean:3:0-3:7: error: declaration body is missing

6
tests/lean/tokenErrors.lean.expected.out
View file

@ -3,4 +3,10 @@ tokenErrors.lean:4:9: error: invalid escape sequence
tokenErrors.lean:7:7: error: unterminated string literal
tokenErrors.lean:10:11: error: unterminated identifier escape
tokenErrors.lean:14:0: error: unterminated comment
tokenErrors.lean:13:0-13:3: error: unexpected doc string
failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
tokenErrors.lean:17:0: error: unterminated comment
inductive Nat : Type
constructors:
Nat.zero : Nat
Nat.succ : Nat → Nat

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

@ -1,5 +1,15 @@
unknownTactic.lean:3:3: error: unknown tactic
unknownTactic.lean:1:41-3:8: error: unsolved goals
x : Nat
a✝ : x = x
⊢ x = x
---
unknownTactic.lean:8:17: error: unknown tactic
unknownTactic.lean:8:2-8:19: error: unsolved goals
x : Nat
⊢ x = x
---
unknownTactic.lean:14:17: error: unknown tactic
unknownTactic.lean:14:2-14:19: error: unsolved goals
x : Nat
⊢ x = x

2
tests/lean/weirdmacro.lean.expected.out
View file

@ -1,4 +1,6 @@
weirdmacro.lean:1:6: error: expected no space before ':' or string literal
weirdmacro.lean:1:0-1:5: error: unexpected syntax
failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
weirdmacro.lean:1:30-1:32: error: elaboration function for 'antiquot' has not been implemented
weirdmacro.lean:1:32: error: expected command
weirdmacro.lean:3:7-3:11: error: unknown identifier 'term'