Inductive array (T:Type) : nat -> Type :=
| empty : array T O
| ext : forall n, T -> array T n -> array T (S n).

Implicit Arguments empty [T].
Implicit Arguments ext [T n].

Notation "x ; y" := (ext x y) (at level 90, right associativity).
Notation " $ " := empty.

Check (5 ; 10 ; 30 ; $).