blob: 6780d63a04db4201140664b1aa56153d570f73f3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* Check notations for sigma types *)
Check { 0 = 0 } + { 0 < 1 }.
Check (0 = 0) + { 0 < 1 }.
Check { x | x = 1 }.
Check { x | x = 1 & 0 < x }.
Check { x : nat | x = 1 }.
Check { x : nat | x = 1 & 0 < x }.
Check { x & x = 1 }.
Check { x & x = 1 & 0 < x }.
Check { x : nat & x = 1 }.
Check { x : nat & x = 1 & 0 < x }.
Check {'(x,y) | x = 1 }.
Check {'(x,y) | x = 1 & y = 0 }.
Check {'(x,y) : nat * nat | x = 1 }.
Check {'(x,y) : nat * nat | x = 1 & y = 0 }.
Check {'(x,y) & x = 1 }.
Check {'(x,y) & x = 1 & y = 0 }.
Check {'(x,y) : nat * nat & x = 1 }.
Check {'(x,y) : nat * nat & x = 1 & y = 0 }.
|
