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

chore(tests): update tests to new position information for by tac

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-30 11:17:46 -05:00
parent 000d97a9a6
commit d542e95d20
9 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/attribute_bug1.lean.expected.out
View file

@ -1,9 +1,9 @@
attribute_bug1.lean:7:0: error: simplify tactic failed to simplify
attribute_bug1.lean:7:3: error: simplify tactic failed to simplify
state:
n : ℕ
⊢ f n = n + 1
constant fdef : ∀ (n : ℕ), f n = n + 1
attribute_bug1.lean:19:0: error: simplify tactic failed to simplify
attribute_bug1.lean:19:3: error: simplify tactic failed to simplify
state:
n : ℕ
⊢ f n = n + 1

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

@ -8,7 +8,7 @@ a_1 : ¬¬a = b,
H : ¬a = b
⊢ false
-------
by_contradiction.lean:22:0: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
by_contradiction.lean:22:3: error: tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)
state:
p q : Prop,
a : ¬¬p

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

@ -1,4 +1,4 @@
ctx_error_msgs.lean:4:0: error: infer type failed, function expected at
ctx_error_msgs.lean:4:3: error: infer type failed, function expected at
f a
term
f
@ -7,16 +7,16 @@ has type
state:
f a : ℕ
⊢ true
ctx_error_msgs.lean:11:0: error: infer type failed, unknown variable
ctx_error_msgs.lean:11:3: error: infer type failed, unknown variable
a
state:
⊢ true
ctx_error_msgs.lean:18:0: error: infer type failed, incorrect number of universe levels
ctx_error_msgs.lean:18:3: error: infer type failed, incorrect number of universe levels
eq
state:
a : ℕ
⊢ true
ctx_error_msgs.lean:23:0: error: infer type failed, incorrect number of universe levels
ctx_error_msgs.lean:23:3: error: infer type failed, incorrect number of universe levels
eq.{0 0}
state:
a : ℕ

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

@ -8,7 +8,7 @@ x : ℕ := ?m_1
--- inside focus tac ---
a : ℕ
⊢ ℕ
focus_tac.lean:4:0: error: focus tactic failed, focused goal has not been solved
focus_tac.lean:4:3: error: focus tactic failed, focused goal has not been solved
state:
a : ℕ
⊢ ℕ

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

@ -1,4 +1,4 @@
format_thunk1.lean:4:0: error: invalid definev tactic, value has type
format_thunk1.lean:4:3: error: invalid definev tactic, value has type
ℕ
but is expected to have type
string

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

@ -1,4 +1,4 @@
set_attr1.lean:14:0: error: tactic failed, there are unsolved goals
set_attr1.lean:14:3: error: tactic failed, there are unsolved goals
state:
n : ℕ
⊢ f n = n + 1

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

@ -1,4 +1,4 @@
subst_bug.lean:4:0: error: tactic failed, there are unsolved goals
subst_bug.lean:4:3: error: tactic failed, there are unsolved goals
state:
b2 : bool
⊢ ff && b2 = ff

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

@ -1,4 +1,4 @@
tactic_failure.lean:4:0: error: assumption tactic failed
tactic_failure.lean:4:3: error: assumption tactic failed
state:
A B : Type,
Hb : B

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

@ -1,4 +1,4 @@
unify_tac1.lean:12:0: error: is_def_eq failed
unify_tac1.lean:12:3: error: is_def_eq failed
state:
A : Type,
a : A,