forked from coq/coq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
activation.out
73 lines (73 loc) · 2.69 KB
/
activation.out
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
The following notations have been disabled:
Notation "x + y" := (Nat.add x y) : nat_scope
File "./output/activation.v", line 5, characters 0-47:
The command has indeed failed with message:
More than one interpretation bound to this notation, confirm with the "all"
modifier.
The following notations have been disabled:
Notation "x * y" := (Nat.mul x y) : nat_scope
Notation "x * y" := (Nat.mul x y) (in custom foo)
The following notations have been enabled:
Notation "x * y" := (Nat.mul x y) : nat_scope
The following notations have been disabled:
Notation "'exists2' x : A , p & q" := (ex2 (fun x => p) (fun x => q))
: type_scope
Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
: type_scope
Notation "'exists2' ' x : A , p & q" := (ex2 (fun x => p) (fun x => q))
: type_scope
Notation "'exists2' ' x , p & q" := (ex2 (fun x => p) (fun x => q))
: type_scope
The following notations have been disabled:
Notation "x <= y <= z" := (and (le x y) (le y z)) : nat_scope
Notation "x <= y < z" := (and (le x y) (lt y z)) : nat_scope
Notation "n <= m" := (le n m) : nat_scope
Notation "x < y <= z" := (and (lt x y) (le y z)) : nat_scope
The following notations have been disabled:
Notation "x >= y" := (ge x y) : nat_scope
Notation "x > y" := (gt x y) : nat_scope
Notation "x < y < z" := (and (lt x y) (lt y z)) : nat_scope
Notation "x < y" := (lt x y) : nat_scope
Notation "x - y" := (Nat.sub x y) : nat_scope
Notation "x * y" := (Nat.mul x y) : nat_scope
File "./output/activation.v", line 12, characters 0-22:
The command has indeed failed with message:
No notation provided.
File "./output/activation.v", line 15, characters 0-24:
The command has indeed failed with message:
Found no matching notation to enable or disable.
The following notations have been disabled:
Notation activation.Abbrev.f w := (S w)
The following notations have been enabled:
Notation activation.Abbrev.f w := (S w)
The following notations have been disabled:
Notation activation.Abbrev.A.a := Prop
a
: Type
The following notations have been disabled:
Notation activation.Abbrev.a := Prop
File "./output/activation.v", line 24, characters 11-12:
The command has indeed failed with message:
The reference a was not found in the current environment.
Prop
: Type
The following notations have been enabled:
Notation activation.Abbrev.a := Prop
Notation activation.Abbrev.A.a := Prop
a
: Type
a
: Type
0
: nat
The following notations have been disabled:
Notation activation.Abbrev.x := 0
x
: bool
The following notations have been enabled:
Notation activation.Abbrev.x := 0
0
: nat
File "./output/activation.v", line 44, characters 0-49:
The command has indeed failed with message:
Found no matching notation to enable or disable.