blob: 3ab3de4571a8f351fa8eb3fd485a172d292ca811 (
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
|
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
|
