let array_size_t = (n: SZ.t { SZ.v n > 0 })
let array_size_t =
(n: SZ.t{SZ.v n > 0})
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
FStar.SizeT.t Prims.b2t Prims.op_GreaterThan FStar.SizeT.v
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
val array_size_t : Type0
Type0