val larray : t: Type0 -> n: FStar.UInt32.t -> Type0
let larray t (n:U32.t) = A.larray t (U32.v n)
module Zeta.Steel.Util
open Steel.ST.Util
module A = Steel.ST.Array
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast

let full = Steel.FractionalPermission.full_perm
/
Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked
Zeta.Steel.Util.fst
t: Type0 -> n: FStar.UInt32.t -> Type0
FStar.UInt32.t Steel.ST.Array.larray FStar.UInt32.v
let larray t (n: U32.t) =
  
A.larray t (U32.v n)