Inductive indexTypeT : Set :=
  (** Index values are 8-bit unsigned integers. *)
  | INDEX_8
  (** Index values are 16-bit unsigned integers. *)
  | INDEX_16
  (** Index values are 32-bit unsigned integers. *)
  | INDEX_32
  .
