1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
1 goal
f : nat -> nat
x : X
============================
{| A := A x; B := f (B x); C := C x |} =
{| A := A x; B := f (B x); C := C x |}
1 goal
x : X
============================
3 = 3
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
(set Nat.add)
More precisely:
- ?Setter: Cannot infer the implicit parameter Setter of set whose type is
"Setter Nat.add" (no type class instance found).
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
(set get_A)
More precisely:
- ?Setter: Cannot infer the implicit parameter Setter of set whose type is
"Setter get_A" (no type class instance found).
The command has indeed failed with message:
In environment
x : several_nats
The term "Build_several_nats (nat1 x) (nat3 x)" has type
"nat -> several_nats"
while it is expected to have type "several_nats".
The command has indeed failed with message:
Tactic failure: incorrect settable! declaration (perhaps fields are out-of-order?).
The command has indeed failed with message:
Tactic failure: incorrect settable! declaration (perhaps fields are out-of-order?).
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
(fun (f : nat -> nat) (x : several_nats) => x <| nat1 ::= f |>)
More precisely:
- ?Setter: Cannot infer the implicit parameter Setter of set whose type is
"Setter nat1" (no type class instance found) in
environment:
f : nat -> nat
x : several_nats
|
