blob: d2605175893d301cc06a8425603e74741b3eb35f (
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
|
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
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
|