diff options
Diffstat (limited to 'test-suite/output/prim_array.v')
| -rw-r--r-- | test-suite/output/prim_array.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/prim_array.v b/test-suite/output/prim_array.v new file mode 100644 index 0000000000..a82f6a16f1 --- /dev/null +++ b/test-suite/output/prim_array.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Check [| | 0 |]. + +Check [| 1; 2; 3 | 0 |]. + +Set Printing Universes. +Check [| | 0 |]. + +Check [| bool; list nat | nat |]. |