let vale_heap = vale_heap
let vale_heap =
vale_heap
Vale.X64.Memory.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapTypes_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.BigOps.fsti.checked
Vale.X64.Memory.fsti
Vale.Arch.HeapImpl.vale_heap
module Vale.X64.Memory
include Vale.Arch.HeapTypes_s
open FStar.Mul
open Vale.Def.Prop_s
open Vale.X64.Machine_s
open Vale.Arch.HeapImpl
module Map16 = Vale.Lib.Map16
val vale_heap : Type
Type