val heap_impl : Type u#1
let heap_impl = vale_full_heap
val heap_impl : Type u#1
let heap_impl =
vale_full_heap
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.HeapImpl.vale_full_heap
module Vale.Arch.Heap
open FStar.Mul
open Vale.Interop
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16
friend Vale.Arch.HeapImpl
val heap_impl : Type u#1
Type