test-suite/bugs/closed/bug_13354.v


1
2
3
4
5
6
7
8
9
10

Primitive array := #array_type.

Definition testArray : array nat := [| 1; 2; 4 | 0 : nat |].

Definition on_array {A:Type} (x:array A) : Prop := True.

Check on_array testArray.

Check @on_array nat testArray.