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

chore(tests): changed sorry warnings

Browse source
This commit is contained in:
Gabriel Ebner 2017-02-28 15:01:01 +01:00
parent d22bfbd12a
commit 176fb9c81f
48 changed files with 50 additions and 90 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/1162.lean.expected.out
View file

@ -1,2 +1 @@
1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
1162.lean:7:4: warning: declaration 'ppday' uses sorry

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

@ -5,4 +5,4 @@ new_ax
(a, a)
1299.lean:13:8: error: invalid theorem 'd2', theorems should not depend on axioms introduced using tactics (solution: mark theorem as a definition)
theorem d2 : true = true :=
[incorrect proof]
sorry

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

@ -1,7 +1,7 @@
1369.lean:15:8: warning: declaration '_example' uses sorry
1369.lean:15:0: warning: declaration '[anonymous]' uses sorry
17 ≤ 555555
⊢ 17 ≤ 555555
1369.lean:21:8: warning: declaration '_example' uses sorry
1369.lean:21:0: warning: declaration '[anonymous]' uses sorry
?m_1 ≤ 555555
⊢ ?m_1 ≤ 555555
1369.lean:33:8: warning: declaration '_example' uses sorry
1369.lean:33:0: warning: declaration '[anonymous]' uses sorry

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

@ -1,6 +1,6 @@
(1, 2) : ℕ × ℕ
and.intro trivial trivial : true ∧ true
anc1.lean:5:8: warning: declaration '_example' uses sorry
anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry
⟨1, sorry⟩ : Σ' (x : ℕ), x > 0
show true, from true.intro : true
Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0

1
tests/lean/assertion1.lean.expected.out
View file

@ -1,2 +1 @@
assertion1.lean:37:21: error: invalid '^.' notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...)
assertion1.lean:35:11: warning: declaration 'tensor_on_left' uses sorry

1
tests/lean/aux_decl_zeta.lean.expected.out
View file

@ -8,4 +8,3 @@ has type
vec ℕ n
but is expected to have type
vec ℕ 10
aux_decl_zeta.lean:5:11: warning: declaration 'f' uses sorry

1
tests/lean/bad_error2.lean.expected.out
View file

@ -7,4 +7,3 @@ _match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
w : ℕ,
hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
⊢ n + w = m
bad_error2.lean:3:8: warning: declaration '_example' uses sorry

1
tests/lean/bad_error3.lean.expected.out
View file

@ -10,4 +10,3 @@ bad_error3.lean:7:0: error: tactic failed, there are unsolved goals
state:
p : ℕ → ℕ → Prop
⊢ sorry
bad_error3.lean:5:4: warning: declaration 'ex' uses sorry

1
tests/lean/bad_error4.lean.expected.out
View file

@ -4,4 +4,3 @@ has type
Π (a : unit) (b : delayed[?m_1]), delayed[?m_2]
but is expected to have type
unit → unit
bad_error4.lean:4:11: warning: declaration 'bar' uses sorry

1
tests/lean/bad_error5.lean.expected.out
View file

@ -5,4 +5,3 @@ c : S
bad_error5.lean:13:10: error: failed to add declaration '_interaction' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
…
bad_error5.lean:9:11: warning: declaration 'V' uses sorry

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

@ -1,10 +1,7 @@
bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
bad_inaccessible.lean:2:11: warning: declaration 'f1' uses sorry
bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
b
but is expected to be
a
bad_inaccessible.lean:5:11: warning: declaration 'f2' uses sorry
bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
.?m_1 + 1
bad_inaccessible.lean:12:11: warning: declaration 'foo' uses sorry

1
tests/lean/bad_inaccessible2.lean.expected.out
View file

@ -7,4 +7,3 @@ has type
but is expected to have type
vec A .(.?m_2 + 1)
bad_inaccessible2.lean:31:46: error: ill-formed match/equations expression
bad_inaccessible2.lean:29:11: warning: declaration 'map_head' uses sorry

1
tests/lean/cls_err.lean.expected.out
View file

@ -1,4 +1,3 @@
cls_err.lean:13:2: error: failed to synthesize type class instance for
A : Type u
⊢ H A
cls_err.lean:12:13: warning: declaration 'tst' uses sorry

1
tests/lean/crash.lean.expected.out
View file

@ -16,4 +16,3 @@ P : Prop,
H : P,
H' : ¬P
⊢ sorry
crash.lean:6:11: warning: declaration 'crash' uses sorry

1
tests/lean/ctx.lean.expected.out
View file

@ -6,4 +6,3 @@ b1 b2 b3 : bool,
h : A = B,
p1 p2 : A × B
⊢ ℕ
ctx.lean:2:11: warning: declaration 'foo' uses sorry

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

@ -8,7 +8,7 @@ but is expected to have type
?m_1 → ?m_2 → ?m_4
Additional information:
elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim' uses sorry
elab_error_msgs.lean:4:0: warning: declaration 'bogus_elim' uses sorry
elab_error_msgs.lean:9:0: error: type mismatch at application
bogus_elim trivial
term

1
tests/lean/elab_error_recovery.lean.expected.out
View file

@ -35,7 +35,6 @@ elab_error_recovery.lean:8:29: error: don't know how to synthesize placeholder
context:
half_baked : ℕ → ℕ
⊢ ℕ
elab_error_recovery.lean:1:4: warning: declaration 'half_baked' uses sorry
def half_baked._main : ℕ → ℕ :=
λ (a : ℕ),
ite (a = 3) 2

1
tests/lean/empty.lean.expected.out
View file

@ -1,3 +1,2 @@
empty.lean:6:39: error: failed to synthesize type class instance for
⊢ nonempty Empty
empty.lean:6:25: warning: declaration 'v2' uses sorry

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

@ -3,11 +3,9 @@ context:
f : ℕ → ℕ
⊢ ℕ
eqn_hole.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
eqn_hole.lean:2:11: warning: declaration 'f' uses sorry
eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
context:
g : ℕ → ℕ,
n : ℕ
⊢ ℕ
eqn_hole.lean:6:11: error: support for well-founded recursion has not been implemented yet, use 'set_option trace.eqn_compiler true' for additional information
eqn_hole.lean:6:11: warning: declaration 'g' uses sorry

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

@ -1,6 +1,6 @@
error_pos.lean:1:39: error: type expected at
B
error_pos.lean:1:8: warning: declaration '_example' uses sorry
error_pos.lean:1:0: warning: declaration '[anonymous]' uses sorry
error_pos.lean:4:43: error: type expected at
B
error_pos.lean:9:40: error: type expected at

1
tests/lean/eval_expr_error.lean.expected.out
View file

@ -5,7 +5,6 @@ A : Type,
tst1 : tactic unit,
a : expr
⊢ Type
eval_expr_error.lean:3:9: warning: declaration 'tst1' uses sorry
eval_expr_error.lean:8:0: error: invalid eval_expr, type mismatch
state:
⊢ true

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

@ -8,7 +8,6 @@ but is expected to have type
ℕ
state:
⊢ ℕ
exact_error_pos.lean:4:4: warning: declaration 'ex1' uses sorry
exact_error_pos.lean:15:14: error: type mismatch at application
f 0 tt
term
@ -19,4 +18,3 @@ but is expected to have type
ℕ
state:
⊢ ℕ
exact_error_pos.lean:12:4: warning: declaration 'ex₂' uses sorry

1
tests/lean/hole_in_fn.lean.expected.out
View file

@ -2,4 +2,3 @@ hole_in_fn.lean:6:13: error: don't know how to synthesize placeholder
context:
n : ℕ
⊢ ℕ
hole_in_fn.lean:5:11: warning: declaration 'f' uses sorry

5
tests/lean/hole_issue2.lean.expected.out
View file

@ -1,4 +1,4 @@
hole_issue2.lean:12:25: warning: declaration 'count' uses sorry
hole_issue2.lean:12:0: warning: declaration 'count' uses sorry
hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
context:
A : Type,
@ -10,7 +10,6 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
w : A,
hw : ¬list.count w l₁ ≤ list.count w l₂
⊢ false
hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1' uses sorry
hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
context:
A : Type,
@ -20,7 +19,6 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
H : subcount l₁ l₂ = ff,
h : ⟦l₁⟧ ⊆ ⟦l₂⟧
⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2' uses sorry
hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
context:
A : Type,
@ -30,4 +28,3 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
H : subcount l₁ l₂ = ff,
h : ⟦l₁⟧ ⊆ ⟦l₂⟧
⊢ false
hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3' uses sorry

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

@ -3,7 +3,6 @@ inaccessible.lean:14:10: error: function expected at
inaccessible.lean:14:2: error: invalid occurrence of macro expression in pattern (possible solution, mark term as inaccessible using '.( )')
sorry
inaccessible.lean:14:17: error: ill-formed match/equations expression
inaccessible.lean:13:11: warning: declaration 'inv_3' uses sorry
inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
inaccessible.lean:28:3: error: function expected at
@ -17,8 +16,6 @@ has type
but is expected to have type
imf f sorry
inaccessible.lean:28:16: error: ill-formed match/equations expression
inaccessible.lean:27:11: warning: declaration 'inv_7' uses sorry
inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
.?m_1 + 1
inaccessible.lean:80:11: warning: declaration 'map_6' uses sorry

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

@ -3,9 +3,7 @@ inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided te
f sorry
but is expected to be
f a
inaccessible2.lean:4:11: warning: declaration 'inv_1' uses sorry
inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
inaccessible2.lean:11:39: error: invalid expression, `)` expected
inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
inaccessible2.lean:14:20: error: ill-formed match/equations expression
inaccessible2.lean:13:11: warning: declaration 'symm' uses sorry

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

@ -3,16 +3,13 @@ A : Type ?,
a : A,
this : has_add A
⊢ has_add A
instance_cache1.lean:1:11: warning: declaration 'f1' uses sorry
instance_cache1.lean:6:7: error: failed to synthesize type class instance for
A : Type ?,
a : A,
s : has_add A
⊢ has_add A
instance_cache1.lean:5:11: warning: declaration 'f2' uses sorry
instance_cache1.lean:9:19: error: failed to synthesize type class instance for
A : Type ?,
a : A,
s : has_add A
⊢ has_add A
instance_cache1.lean:8:11: warning: declaration 'f3' uses sorry

10
tests/lean/interactive/1313.lean.expected.out
View file

@ -1,8 +1,8 @@
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":34,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":34,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"ok","seq_num":4}
{"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":11}

8
tests/lean/interactive/complete_field.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"},"response":"additional_message"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n h y\nwhich has type\n p y ∧ q y"},{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5}
{"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9}

24
tests/lean/interactive/complete_import.lean.expected.out
View file

@ -1,15 +1,15 @@
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: bar\ncould not resolve import: bar"},"response":"additional_message"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: bar\ncould not resolve import: bar"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"response":"ok","seq_num":2}
{"prefix":"","response":"ok","seq_num":4}

2
tests/lean/interactive/complete_scanner_error.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msg":{"caption":"","file_name":"f","pos_col":9,"pos_line":4,"severity":"error","text":"unexpected token"},"response":"additional_message"}
{"msgs":[{"caption":"","file_name":"f","pos_col":9,"pos_line":4,"severity":"error","text":"unexpected token"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"prefix":"","response":"ok","seq_num":2}

6
tests/lean/interactive/complete_tactic.lean.expected.out
View file

@ -1,6 +1,6 @@
{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},"response":"additional_message"}
{"msg":{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},"response":"additional_message"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"f","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"f","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"prefix":"","response":"ok","seq_num":2}
{"prefix":"","response":"ok","seq_num":5}

2
tests/lean/interactive/do_info.lean.expected.out
View file

@ -1,4 +1,4 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"tactic.intro","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
{"record":{"full-id":"tactic.transitivity","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"opt_param transparency transparency.semireducible → tactic unit"},"response":"ok","seq_num":9}

2
tests/lean/interactive/info.lean.expected.out
View file

@ -1,4 +1,4 @@
{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"},"response":"additional_message"}
{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[reducible]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":},"response":"ok","seq_num":2}
{"record":{"doc":"reducible"},"response":"ok","seq_num":5}

2
tests/lean/interactive/my_tac_class.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":58,"severity":"information","text":"test\n"},"response":"additional_message"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":58,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":,"state":"Custom state: 2\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":62}

4
tests/lean/interactive/nested_traces.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"},"response":"additional_message"}
{"msg":{"caption":"trace output","file_name":"f","pos_col":23,"pos_line":6,"severity":"information","text":"test\n"},"response":"additional_message"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"},{"caption":"trace output","file_name":"f","pos_col":23,"pos_line":6,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}

8
tests/lean/interactive/rb_map_ts.lean.expected.out
View file

@ -1,7 +1,7 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},"response":"additional_message"}
{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},"response":"additional_message"}
{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"},"response":"additional_message"}
{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":85,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},"response":"additional_message"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":85,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":63}
{"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":67}

4
tests/lean/interactive/trace.lean.expected.out
View file

@ -1,3 +1,3 @@
{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":3,"severity":"information","text":"foo\n"},"response":"additional_message"}
{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":5,"severity":"information","text":"hello world\n"},"response":"additional_message"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":3,"severity":"information","text":"foo\n"}],"response":"all_messages"}
{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":3,"severity":"information","text":"foo\n"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":5,"severity":"information","text":"hello world\n"}],"response":"all_messages"}
{"message":"file invalidated","response":"ok","seq_num":0}

1
tests/lean/meta_equation_pos.lean.expected.out
View file

@ -4,5 +4,4 @@ has type
bool
but is expected to have type
ℕ
meta_equation_pos.lean:1:9: warning: declaration 'f' uses sorry
ℕ : Type

1
tests/lean/minimize_errors.lean.expected.out
View file

@ -4,7 +4,6 @@ has type
ℕ → ℕ
but is expected to have type
ℕ → ℕ → ℕ
minimize_errors.lean:1:4: warning: declaration 'f' uses sorry
f : ℕ → ℕ → ℕ
g : ℕ → ℕ → ℕ
def g : ℕ → ℕ → ℕ :=

1
tests/lean/no_meta_rec_inst.lean.expected.out
View file

@ -3,4 +3,3 @@ no_meta_rec_inst.lean:5:3: error: tactic.mk_instance failed to generate instance
state:
n_has_false : has_false ℕ
⊢ has_false ℕ
no_meta_rec_inst.lean:4:9: warning: declaration 'n_has_false' uses sorry

1
tests/lean/non_exhaustive_error.lean.expected.out
View file

@ -1,2 +1 @@
non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
non_exhaustive_error.lean:2:11: warning: declaration 'f' uses sorry

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

@ -1,4 +1,4 @@
print_ax3.lean:13:6: warning: declaration 'foo5' uses sorry
print_ax3.lean:13:0: warning: declaration 'foo5' uses sorry
no axioms
------
quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b

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

@ -1,2 +1,2 @@
λ (x : A), f x
quot_bug.lean:8:8: warning: declaration '_example' uses sorry
quot_bug.lean:8:0: warning: declaration '[anonymous]' uses sorry

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

@ -2,4 +2,3 @@ set_attr1.lean:14:3: error: tactic failed, there are unsolved goals
state:
n : ℕ
⊢ f n = n + 1
set_attr1.lean:13:11: warning: declaration 'ex2' uses sorry

1
tests/lean/structure_instance_bug.lean.expected.out
View file

@ -1,2 +1 @@
structure_instance_bug.lean:11:0: error: invalid structure value {...}, field 'B' is implicit and must not be provided
structure_instance_bug.lean:10:11: warning: declaration 'foo3' uses sorry

1
tests/lean/structure_instance_bug2.lean.expected.out
View file

@ -1,2 +1 @@
structure_instance_bug2.lean:4:0: error: invalid structure instance, 'default_smt_pre_config' is not the name of a structure type
structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1' uses sorry

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

@ -1,8 +1,8 @@
vm_sorry.lean:1:4: warning: declaration 'half_baked' uses sorry
vm_sorry.lean:1:0: warning: declaration 'half_baked' uses sorry
42
vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry
vm_sorry.lean:12:0: error: undefined
(some nat)
vm_sorry.lean:18:8: warning: declaration '_example' uses sorry
vm_sorry.lean:19:8: warning: declaration '_example' uses sorry
vm_sorry.lean:20:8: warning: declaration '_example' uses sorry
vm_sorry.lean:18:0: warning: declaration '[anonymous]' uses sorry
vm_sorry.lean:19:0: warning: declaration '[anonymous]' uses sorry
vm_sorry.lean:20:0: warning: declaration '[anonymous]' uses sorry