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
|
[< 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
Let "x" e1 e2
: expr
Let "x" e1 e2
: expr
Let "x" e1 e2 : list string
: list string
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
b = a
: Prop
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 226, 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 239, characters 0-60:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing]
File "stdin", line 243, characters 0-64:
Warning: Notation "_ %%% _" was already defined with a different format.
[notation-incompatible-format,parsing]
File "stdin", line 248, 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 276, characters 0-61:
Warning: The format modifier is irrelevant for only parsing rules.
[irrelevant-format-only-parsing,parsing]
File "stdin", line 280, 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 297, 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
|
