blob: be4cd4faea0b6fdde7cba4c02fdfc65a8f7bb0fb (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
|
true ? 0; 1
: nat
if true as x return (x ? nat; bool) then 0 else true
: true ? nat; bool
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
|
