val array_upd (#t: Type) (a: array t) : Tot (Gen.array_upd_t (array_pts_to a))
let array_upd
  (#t: Type)
  (a: array t)
: Tot (Gen.array_upd_t (array_pts_to a))
= fun s n i x ->
    upd a i x;
    return _
val array_upd (#t: Type) (a: array t) : Tot (Gen.array_upd_t (array_pts_to a))
let array_upd (#t: Type) (a: array t) : Tot (Gen.array_upd_t (array_pts_to a)) =
fun s n i x ->
  upd a i x;
  return _
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 FStar.SizeT.t Steel.ST.Util.return FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm FStar.Ghost.reveal Steel.Effect.Common.vprop FStar.Seq.Base.upd FStar.SizeT.v Prims.unit Steel.ST.Array.upd Steel.ST.GenArraySwap.array_upd_t Steel.ST.Array.Swap.array_pts_to
module Steel.ST.Array.Swap
open Steel.ST.GenElim
open Steel.ST.Array // for pts_to

module Gen = Steel.ST.GenArraySwap

[@@__reduce__]
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)

inline_for_extraction
let array_index
  (#t: Type)
  (a: array t)
: Tot (Gen.array_index_t (array_pts_to a))
= fun s n i ->
    index a i

inline_for_extraction
let array_upd
  (#t: Type)
  (a: array t)
val array_upd (#t: Type) (a: array t) : Tot (Gen.array_upd_t (array_pts_to a))
a: Steel.ST.Array.array t -> Steel.ST.GenArraySwap.array_upd_t (Steel.ST.Array.Swap.array_pts_to a)