val array_index (#t: Type) (a: array t) : Tot (Gen.array_index_t (array_pts_to a))
let array_index
  (#t: Type)
  (a: array t)
: Tot (Gen.array_index_t (array_pts_to a))
= fun s n i ->
    index a i
val array_index (#t: Type) (a: array t) : Tot (Gen.array_index_t (array_pts_to a))
let array_index (#t: Type) (a: array t) : Tot (Gen.array_index_t (array_pts_to a)) =
fun s n i -> index a i
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.Array.index Steel.FractionalPermission.full_perm Steel.ST.GenArraySwap.array_index_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)
val array_index (#t: Type) (a: array t) : Tot (Gen.array_index_t (array_pts_to a))
a: Steel.ST.Array.array t
  -> Steel.ST.GenArraySwap.array_index_t (Steel.ST.Array.Swap.array_pts_to a)