blob: 4db5c2d16164eddb2743dba981259fd933d3a74e (
plain)
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
|
The command has indeed failed with message:
In environment
x : T
T : Type
a : T
Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
"?X" because "T" is not in its scope: available arguments are
"x" "C a").
The command has indeed failed with message:
The term "id" has type "ID" while it is expected to have type
"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
1 focused goal
(shelved: 1)
H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal
(shelved: 1)
H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal
(shelved: 1)
H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal
(shelved: 1)
H : forall x : nat, S x = x
============================
?y = 0
|
