val create_post: #a: Type0 -> s: seq a -> heap -> array a -> heap -> Type0
let create_post (#a:Type0) (s:seq a)
: heap -> array a -> heap -> Type0
= fun h0 x h1 ->
  x `unused_in` h0 /\
  contains h1 x /\
  modifies Set.empty h0 h1 /\
  sel h1 x== s
val create_post: #a: Type0 -> s: seq a -> heap -> array a -> heap -> Type0
let create_post (#a: Type0) (s: seq a) :  heap -> array a -> heap -> Type0 =
fun h0 x h1 -> x `unused_in` h0 /\ contains h1 x /\ modifies Set.empty h0 h1 /\ sel h1 x == s
FStar.Array.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Ref.fst.checked FStar.Pervasives.fsti.checked FStar.Heap.fst.checked FStar.All.fst.checked
FStar.Array.fsti
FStar.Seq.Base.seq FStar.Monotonic.Heap.heap FStar.Array.array Prims.l_and FStar.Array.unused_in FStar.Array.contains FStar.Monotonic.Heap.modifies FStar.Set.empty Prims.nat Prims.eq2 FStar.Array.sel
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module FStar.Array

(**
F* standard library mutable arrays module.

@summary Mutable arrays
*)

open FStar.All
open FStar.Seq
open FStar.Ref

#set-options "--max_fuel 0 --initial_fuel 0 --initial_ifuel 0 --max_ifuel 0"

val array (a:Type0) : Type0

val as_ref (#a:Type0) (arr:array a) : GTot (ref (seq a))

let sel (#a:Type0) (h:heap) (s:array a) : GTot (seq a) = Heap.sel h (as_ref s)

let contains (#a:Type0) (h:heap) (s:array a) : Type0 = Heap.contains h (as_ref s)

let unused_in (#a:Type0) (arr:array a) (h:heap) : Type0 = Heap.unused_in (as_ref arr) h

let heap_upd (#a:Type0) (h:heap) (r:array a) (v:seq a) : GTot heap = Heap.upd h (as_ref r) v

let addr_of (#a:Type0) (arr:array a) : GTot nat = addr_of (as_ref arr)

let only (#a:Type0) (arr:array a) : GTot (Set.set nat) = Set.singleton (addr_of arr)

val op_At_Bar (#a:Type0) (s1:array a) (s2:array a)
  : ST (array a)
       (requires (fun h -> contains h s1 /\ contains h s2))
       (ensures  (fun h0 s h1 -> contains h0 s1 /\ contains h0 s2 /\ contains h1 s /\
                              sel h1 s == Seq.append (sel h0 s1) (sel h0 s2) /\
                              modifies Set.empty h0 h1))

unfold let create_post (#a:Type0) (s:seq a)
val create_post: #a: Type0 -> s: seq a -> heap -> array a -> heap -> Type0

    s: FStar.Seq.Base.seq a ->
    _: FStar.Monotonic.Heap.heap ->
    _: FStar.Array.array a ->
    _: FStar.Monotonic.Heap.heap
  -> Type0