blob: 0e4df87148e81e4383e6e3f822a7249f26da639e (
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
|
{0 = 0} + {0 < 1}
: Set
(0 = 0) + {0 < 1}
: Set
{x : nat | x = 1}
: Set
{x : nat | x = 1 & 0 < x}
: Set
{x : nat | x = 1}
: Set
{x : nat | x = 1 & 0 < x}
: Set
{x : nat & x = 1}
: Set
{x : nat & x = 1 & 0 < x}
: Set
{x : nat & x = 1}
: Set
{x : nat & x = 1 & 0 < x}
: Set
{'(x, _) : nat * ?T | x = 1}
: Type
where
?T : [pat : nat * ?T |- Type] (pat cannot be used)
{'(x, y) : nat * nat | x = 1 & y = 0}
: Set
{'(x, _) : nat * nat | x = 1}
: Set
{'(x, y) : nat * nat | x = 1 & y = 0}
: Set
{'(x, _) : nat * ?T & x = 1}
: Type
where
?T : [pat : nat * ?T |- Type] (pat cannot be used)
{'(x, y) : nat * nat & x = 1 & y = 0}
: Type
{'(x, _) : nat * nat & x = 1}
: Type
{'(x, y) : nat * nat & x = 1 & y = 0}
: Type
|
