val set_vale_heap (vfh: vale_full_heap) (vh: vale_heap) : vale_full_heap
let set_vale_heap (vfh:vale_full_heap) (vh:vale_heap) : vale_full_heap =
  {vfh with vf_heap = vh}
val set_vale_heap (vfh: vale_full_heap) (vh: vale_heap) : vale_full_heap
let set_vale_heap (vfh: vale_full_heap) (vh: vale_heap) : vale_full_heap =
{ vfh with vf_heap = vh }
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.X64.Memory.vale_full_heap Vale.X64.Memory.vale_heap Vale.Arch.HeapImpl.Mkvale_full_heap Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_layout Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets
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

unfold let vale_heap = vale_heap
unfold let vale_full_heap = vale_full_heap
unfold let heaplet_id = heaplet_id

[@va_qattr]
let get_vale_heap (vhi:vale_full_heap) : vale_heap = vhi.vf_heap

[@va_qattr]
val set_vale_heap (vfh: vale_full_heap) (vh: vale_heap) : vale_full_heap
vfh: Vale.X64.Memory.vale_full_heap -> vh: Vale.X64.Memory.vale_heap
  -> Vale.X64.Memory.vale_full_heap