val as_ref (#a:Type0) (#rel:preorder a) (x:mreference a rel)
  :Heap.mref a rel
let as_ref #_ #_ x = MkRef?.ref x
val as_ref (#a:Type0) (#rel:preorder a) (x:mreference a rel)
  :Heap.mref a rel
let as_ref #_ #_ x =
MkRef?.ref x
FStar.Monotonic.HyperStack.fst.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Heap.fsti.checked FStar.Map.fsti.checked FStar.Classical.fsti.checked
FStar.Monotonic.HyperStack.fst
FStar.Preorder.preorder FStar.Monotonic.HyperStack.mreference FStar.Monotonic.HyperStack.__proj__MkRef__item__ref FStar.Monotonic.Heap.mref
(*
   Copyright 2008-2014 Aseem Rastogi, and 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.Monotonic.HyperStack

open FStar.Preorder
module Map = FStar.Map

let map_invariant = map_invariant_predicate

let downward_closed = downward_closed_predicate

let tip_top = tip_top_predicate

let rid_ctr_pred = rid_ctr_pred_predicate

noeq type mem' =
  | HS :rid_ctr:int -> h:hmap -> tip:rid -> mem'

let mk_mem rid_ctr h tip = HS rid_ctr h tip

let get_hmap m = m.h
let get_rid_ctr m = m.rid_ctr
let get_tip m = m.tip

let lemma_mk_mem'_projectors _ _ _ = ()

let lemma_mem_projectors_are_in_wf_relation _ = ()

let lemma_is_wf_ctr_and_tip_intro _ _ _ = root_is_not_freeable ()

let lemma_is_wf_ctr_and_tip_elim _ = ()

let lemma_map_invariant _ _ _ = ()

let lemma_downward_closed _ _ _ = ()

let lemma_tip_top _ _ = ()

let lemma_tip_top_smt _ _ = ()

let lemma_rid_ctr_pred _ = ()
val as_ref (#a:Type0) (#rel:preorder a) (x:mreference a rel)
  :Heap.mref a rel
x: FStar.Monotonic.HyperStack.mreference a rel -> FStar.Monotonic.Heap.mref a rel