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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
|
[< 0 > + < 1 > * < 2 >]
: nat
Entry custom:myconstr is
[ "6" RIGHTA
[ ]
| "5" RIGHTA
[ SELF; "+"; NEXT ]
| "4" RIGHTA
[ SELF; "*"; NEXT ]
| "3" RIGHTA
[ "<"; term LEVEL "10"; ">" ] ]
[< b > + < b > * < 2 >]
: nat
[<< # 0 >>]
: option nat
[b + c]
: nat
fun a : nat => [a + a]
: nat -> nat
[1 {f 1}]
: Expr
fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
: nat -> Expr -> Expr -> Expr
fun e : Expr =>
match e with
| [x y + z] => [x + y z]
| [1 + 1] => [1]
| _ => [e + e]
end
: Expr -> Expr
[(1 + 1)]
: Expr
myAnd1 True True
: Prop
r 2 3
: Prop
let v := 0%test17 in v : myint63
: myint63
fun y : nat => # (x, z) |-> y & y
: forall y : nat,
(?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat)
where
?T : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0
|- Type] (pat, p0, p cannot be used)
?T0 : [y : nat pat : ?T * ?T0 p0 : ?T * ?T0 p := p0 : ?T * ?T0
|- Type] (pat, p0, p cannot be used)
?T1 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
|- Type] (pat, p0, p cannot be used)
?T2 : [y : nat pat : ?T1 * ?T2 p0 : ?T1 * ?T2 p := p0 : ?T1 * ?T2
|- Type] (pat, p0, p cannot be used)
fun y : nat => # (x, z) |-> (x + y) & (y + z)
: forall y : nat,
(nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
where
?T : [y : nat pat : nat * ?T p0 : nat * ?T p := p0 : nat * ?T
|- Type] (pat, p0, p cannot be used)
?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat
|- Type] (pat, p0, p cannot be used)
fun '{| |} => true
: R -> bool
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
Entry custom:expr is
[ "201" RIGHTA
[ "{"; term LEVEL "200"; "}" ] ]
fun x : nat => [ x ]
: nat -> nat
fun x : nat => [x]
: nat -> nat
∀ x : nat, x = x
: Prop
File "stdin", line 187, characters 0-160:
Warning: Notation "∀ _ .. _ , _" was already defined with a different format
in scope type_scope. [notation-incompatible-format,parsing]
∀x : nat,x = x
: Prop
File "stdin", line 200, characters 0-60:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing]
File "stdin", line 204, characters 0-64:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing]
File "stdin", line 209, characters 0-62:
Warning: Lonely notation "_ %%%% _" was already defined with a different
format. [notation-incompatible-format,parsing]
3 %% 4
: nat
3 %% 4
: nat
3 %% 4
: nat
File "stdin", line 237, characters 0-61:
Warning: The format modifier is irrelevant for only parsing rules.
[irrelevant-format-only-parsing,parsing]
File "stdin", line 241, characters 0-63:
Warning: The only parsing modifier has no effect in Reserved Notation.
[irrelevant-reserved-notation-only-parsing,parsing]
fun x : nat => U (S x)
: nat -> nat
V tt
: unit * (unit -> unit)
fun x : nat => V x
: forall x : nat, nat * (?T -> ?T)
where
?T : [x : nat x0 : ?T |- Type] (x0 cannot be used)
File "stdin", line 258, characters 0-30:
Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
0 :=: 0
: Prop
fun x : nat => <{ x; (S x) }>
: nat -> nat
exists p : nat, ▢_p (p >= 1)
: Prop
▢_n (n >= 1)
: Prop
The command has indeed failed with message:
Found an inductive type while a variable name was expected.
The command has indeed failed with message:
Found a constructor while a variable name was expected.
The command has indeed failed with message:
Found a constant while a variable name was expected.
exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
: Prop
▢_n (n >= 1)
: Prop
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
▢_tt (tt = tt)
: Prop
The command has indeed failed with message:
Found a constant while a pattern was expected.
exists x y : nat, ▢_(x, y) (x >= 1 /\ y >= 2)
: Prop
pseudo_force n (fun n : nat => n >= 1)
: Prop
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
▢_tt (tt = tt)
: Prop
The command has indeed failed with message:
Found a constant while a pattern was expected.
exists x y : nat, myforce (x, y) (x >= 1 /\ y >= 2)
: Prop
myforce n (n >= 1)
: Prop
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
myforce tt (tt = tt)
: Prop
The command has indeed failed with message:
Found a constant while a pattern was expected.
id nat
: Set
fun a : bool => id a
: bool -> bool
fun nat : bool => id nat
: bool -> bool
The command has indeed failed with message:
Found an inductive type while a pattern was expected.
!! nat, nat = true
: Prop
!!! nat, nat = true
: Prop
!!!! (nat, id), nat = true /\ id = false
: Prop
∀ x : nat, x = 0
: Prop
∀₁ x, x = 0
: Prop
∀₁ x, x = 0
: Prop
∀₂ x y, x + y = 0
: Prop
((1, 2))
: nat * nat
%% [x == 1]
: Prop
%%% [1]
: Prop
[[2]]
: nat * nat
%%%
: Type
## (x, _) (x = 0)
: Prop
The command has indeed failed with message:
Unexpected type constraint in notation already providing a type constraint.
## '(x, y) (x + y = 0)
: Prop
## x (x = 0)
: Prop
## '(x, y) (x = 0)
: Prop
fun f : ## a (a = 0) => f 1 eq_refl
: ## a (a = 0) -> 1 = 0
|
