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
|
true ? 0; 1
: nat
if true as x return (x ? nat; bool) then 0 else true
: nat
Defining 'proj1' as keyword
fun e : nat * nat => proj1 e
: nat * nat -> nat
Defining 'decomp' as keyword
decomp (true, true) as t, u in (t, u)
: bool * bool
!(0 = 0)
: Prop
forall n : nat, n = 0
: Prop
!(0 = 0)
: Prop
forall n : nat, #(n = n)
: Prop
forall n n0 : nat, ##(n = n0)
: Prop
forall n n0 : nat, ###(n = n0)
: Prop
3 + 3
: Z
3 + 3
: znat
[1; 2; 4]
: list nat
(1; 2, 4)
: nat * nat * nat
Defining 'ifzero' as keyword
ifzero 3
: bool
Defining 'pred' as keyword
pred 3
: nat
fun n : nat => pred n
: nat -> nat
fun n : nat => pred n
: nat -> nat
Defining 'ifn' as keyword
Defining 'is' as keyword
fun x : nat => ifn x is succ n then n else 0
: nat -> nat
1-
: bool
-4
: Z
The command has indeed failed with message:
=> Error: x should not be bound in a recursive pattern of the right-hand side.
The command has indeed failed with message:
=> Error: in the right-hand side, y and z should appear in
term position as part of a recursive pattern.
The command has indeed failed with message:
=> Error: The reference w was not found in the current environment.
The command has indeed failed with message:
=> Error: x is unbound in the right-hand side.
The command has indeed failed with message:
=> Error: in the right-hand side, y and z should appear in
term position as part of a recursive pattern.
The command has indeed failed with message:
=> Error: z is expected to occur in binding position in the right-hand side.
The command has indeed failed with message:
=> Error: as y is a non-closed binder, no such "," is allowed to occur.
The command has indeed failed with message:
=> Error: Cannot find where the recursive pattern starts.
The command has indeed failed with message:
=> Error: Cannot find where the recursive pattern starts.
The command has indeed failed with message:
=> Error: Cannot find where the recursive pattern starts.
The command has indeed failed with message:
=> Error: Cannot find where the recursive pattern starts.
The command has indeed failed with message:
=> Error: Both ends of the recursive pattern are the same.
SUM (nat * nat) nat
: Set
FST (0; 1)
: Z
Nil
: forall A : Type, list A
NIL:list nat
: list nat
Defining 'I' as keyword
(false && I 3)%bool /\ I 6
: Prop
[|1, 2, 3; 4, 5, 6|]
: Z * Z * Z * (Z * Z * Z)
[|0 * (1, 2, 3); (4, 5, 6) * false|]
: Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
: (Z -> Z -> Z -> Z) -> Z
plus
: nat -> nat -> nat
S
: nat -> nat
mult
: nat -> nat -> nat
le
: nat -> nat -> Prop
plus
: nat -> nat -> nat
succ
: nat -> nat
mult
: nat -> nat -> nat
le
: nat -> nat -> Prop
fun x : option Z => match x with
| SOME x0 => x0
| NONE => 0
end
: option Z -> Z
fun x : option Z => match x with
| SOME2 x0 => x0
| NONE2 => 0
end
: option Z -> Z
fun x : option Z => match x with
| SOME3 x0 => x0
| NONE3 => 0
end
: option Z -> Z
|
