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/output/prim_array.v | |
| 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/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 |]. |