val base_array
      (#t #tn: Type0)
      (td: typedef t)
      (n: nat{SZ.fits n /\ n > 0})
      (#[solve_nat_t_of_nat ()] prf: squash (norm norm_typenat (nat_t_of_nat n == tn)))
    : Tot (typedef (base_array_t t tn (SZ.uint_to_t n)))
let base_array (#t: Type0) (#tn: Type0) (td: typedef t) (n: nat {SZ.fits n /\ n > 0}) (# [solve_nat_t_of_nat ()] prf: squash (norm norm_typenat (nat_t_of_nat n == tn))) : Tot (typedef (base_array_t t tn (SZ.uint_to_t n)))
= base_array0 tn td (SZ.uint_to_t n)
val base_array
      (#t #tn: Type0)
      (td: typedef t)
      (n: nat{SZ.fits n /\ n > 0})
      (#[solve_nat_t_of_nat ()] prf: squash (norm norm_typenat (nat_t_of_nat n == tn)))
    : Tot (typedef (base_array_t t tn (SZ.uint_to_t n)))
let base_array
      (#t #tn: Type0)
      (td: typedef t)
      (n: nat{SZ.fits n /\ n > 0})
      (#[solve_nat_t_of_nat ()] prf: squash (norm norm_typenat (nat_t_of_nat n == tn)))
    : Tot (typedef (base_array_t t tn (SZ.uint_to_t n))) =
base_array0 tn td (SZ.uint_to_t 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.Base.typedef Prims.nat Prims.l_and FStar.SizeT.fits Prims.b2t Prims.op_GreaterThan Prims.squash FStar.Pervasives.norm Steel.C.Typenat.norm_typenat Prims.eq2 Steel.C.Typenat.nat_t_of_nat Steel.ST.C.Types.Array.base_array0 FStar.SizeT.uint_to_t Steel.ST.C.Types.Array.base_array_t
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"]
let base_array_index_t (n: array_size_t) : Tot eqtype =
  Steel.ST.C.Types.Array.Base.array_domain (Ghost.hide n)
[@@noextract_to "krml"]
val base_array0 (#t: Type0) (tn: Type0) (td: typedef t) (n: array_size_t) : Tot (typedef (base_array_t t tn n))

inline_for_extraction
[@@noextract_to "krml"] // proof-only
val base_array
      (#t #tn: Type0)
      (td: typedef t)
      (n: nat{SZ.fits n /\ n > 0})
      (#[solve_nat_t_of_nat ()] prf: squash (norm norm_typenat (nat_t_of_nat n == tn)))
    : Tot (typedef (base_array_t t tn (SZ.uint_to_t n)))
td: Steel.ST.C.Types.Base.typedef t -> n: Prims.nat{FStar.SizeT.fits n /\ n > 0}
  -> Steel.ST.C.Types.Base.typedef (Steel.ST.C.Types.Array.base_array_t t
          tn
          (FStar.SizeT.uint_to_t n))