diff options
| author | Gaëtan Gilbert | 2020-11-02 15:03:09 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-02 15:03:09 +0100 |
| commit | 225a4ee2871b58661f9689255237a1e189ee6a4c (patch) | |
| tree | 4901f319b8babc4e5bc24e6a3a3d3fa68cb21e35 /test-suite | |
| parent | 1280a492b87f02aac8c8f8496ebd42039762d7e4 (diff) | |
Nicer spacing when printing array literals
From
[|x; y; z | def : ty |]
to
[| x; y; z | def : ty |]
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/prim_array.out | 9 | ||||
| -rw-r--r-- | test-suite/output/prim_array.v | 10 |
2 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out new file mode 100644 index 0000000000..6c12153ab9 --- /dev/null +++ b/test-suite/output/prim_array.out @@ -0,0 +1,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 *) 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 |]. |