val array_pts_to (#t: Type) (a: array t) : Tot (Gen.array_pts_to_t t)
let array_pts_to (#t: Type) (a: array t) : Tot (Gen.array_pts_to_t t) =
  fun s -> pts_to a full_perm (Ghost.reveal s)
val array_pts_to (#t: Type) (a: array t) : Tot (Gen.array_pts_to_t t)
let array_pts_to (#t: Type) (a: array t) : Tot (Gen.array_pts_to_t t) =
fun s -> pts_to a full_perm (Ghost.reveal s)
Steel.ST.Array.Swap.fst.checked
Steel.ST.GenElim.fsti.checked Steel.ST.GenArraySwap.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.Array.Swap.fst
Steel.ST.Array.array FStar.Ghost.erased FStar.Seq.Base.seq Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm FStar.Ghost.reveal Steel.Effect.Common.vprop Steel.ST.GenArraySwap.array_pts_to_t
module Steel.ST.Array.Swap
open Steel.ST.GenElim
open Steel.ST.Array // for pts_to

module Gen = Steel.ST.GenArraySwap

[@@__reduce__]
val array_pts_to (#t: Type) (a: array t) : Tot (Gen.array_pts_to_t t)
a: Steel.ST.Array.array t -> Steel.ST.GenArraySwap.array_pts_to_t t