val heap_get (hi:heap_impl) : machine_heap
let heap_get hi = hi.vf_heap.mh
val heap_get (hi:heap_impl) : machine_heap
let heap_get hi =
hi.vf_heap.mh
Vale.Arch.Heap.fst.checked
Vale.Lib.Map16.fsti.checked Vale.Interop.fsti.checked Vale.Arch.HeapImpl.fst.checked Vale.Arch.HeapImpl.fst.checked prims.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked
Vale.Arch.Heap.fst
Vale.Arch.Heap.heap_impl Vale.Arch.HeapImpl.__proj__ValeHeap__item__mh Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap Vale.Arch.MachineHeap_s.machine_heap
module Vale.Arch.Heap
open FStar.Mul
open Vale.Interop
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16
friend Vale.Arch.HeapImpl

let heap_impl = vale_full_heap
val heap_get (hi:heap_impl) : machine_heap
hi: Vale.Arch.Heap.heap_impl -> Vale.Arch.MachineHeap_s.machine_heap