blob: 6c12153ab9abe5fa6c46a5acf2ada65a3790aaeb (
plain)
1
2
3
4
5
6
7
8
9
|
[| | 0 : nat |]
: array nat
[| 1; 2; 3 | 0 : nat |]
: array nat
[| | 0 : nat |]@{Set}
: array@{Set} nat
[| bool; list nat | nat : Set |]@{prim_array.4}
: array@{prim_array.4} Set
(* {prim_array.4} |= Set < prim_array.4 *)
|
