|
|
|---|
|
|
|
|---|
Fixtype of Java (unannotated) array types [JLS14:4.3] [JLS14:8.3].
This is a tagged union type, introduced by fty::deftagsum.
An array type consists of an element type and one or more dimensions [JLS14:10.1]. The element type may be a primitive type, a class type, or a type variable, but not an array type: recall the distinction between array components and elements [JLS14:10].
The dimensions are simply captured by a positive integer.
Since the three summands of this fixtype have a field in common, an alternative formalization approach is to define an array type as a product of an array element type and a number of dimensions. We may do that in the future, if it turns out to be more convenient.