val base_array_index_t (n: array_size_t) : Tot eqtype
let base_array_index_t (n: array_size_t) : Tot eqtype =
  Steel.ST.C.Types.Array.Base.array_domain (Ghost.hide n)
val base_array_index_t (n: array_size_t) : Tot eqtype
let base_array_index_t (n: array_size_t) : Tot eqtype =
Steel.ST.C.Types.Array.Base.array_domain (Ghost.hide n)
Steel.ST.C.Types.Array.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Base.fsti.checked Steel.ST.C.Types.Array.Base.fst.checked Steel.FractionalPermission.fst.checked Steel.C.Typenat.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.C.Types.Array.fsti
Steel.ST.C.Types.Array.array_size_t Steel.ST.C.Types.Array.Base.array_domain FStar.Ghost.hide FStar.SizeT.t Prims.eqtype
module Steel.ST.C.Types.Array
open Steel.ST.Util
include Steel.ST.C.Types.Base
open Steel.C.Typenat

module P = Steel.FractionalPermission
module SZ = FStar.SizeT

// To be extracted as: t[tn]
// Per the C standard, base array types must be of nonzero size
inline_for_extraction [@@noextract_to "krml"]
let array_size_t = (n: SZ.t { SZ.v n > 0 })
val base_array_t ([@@@strictly_positive] t: Type0) (tn: Type0 (* using Typenat (or Typestring for `#define`d constants) *)) (n: array_size_t) : Type0
inline_for_extraction [@@noextract_to "krml"]
val base_array_index_t (n: array_size_t) : Tot eqtype
n: Steel.ST.C.Types.Array.array_size_t -> Prims.eqtype