val get_heaplet_id (h:vale_heap) : option heaplet_id
let get_heaplet_id h =
  h.heapletId
val get_heaplet_id (h:vale_heap) : option heaplet_id
let get_heaplet_id h =
h.heapletId
Vale.PPC64LE.Memory.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.MachineHeap_s.fst.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Memory.fst
Vale.Arch.HeapImpl.vale_heap Vale.Arch.HeapImpl.__proj__ValeHeap__item__heapletId FStar.Pervasives.Native.option Vale.Arch.HeapImpl.heaplet_id
module Vale.PPC64LE.Memory
include Vale.Interop.Types
friend Vale.Arch.Heap
open Vale.Def.Opaque_s
open Vale.Arch.HeapImpl
open Vale.Arch.Heap
open Vale.Interop.Base
module IB = Vale.Interop.Base
module I = Vale.Interop
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module M = LowStar.Modifies
open LowStar.ModifiesPat
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
module H = FStar.Heap
module S = Vale.Arch.MachineHeap_s

#reset-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1"

let b8 = IB.b8

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd
val get_heaplet_id (h:vale_heap) : option heaplet_id
h: Vale.Arch.HeapImpl.vale_heap -> FStar.Pervasives.Native.option Vale.Arch.HeapImpl.heaplet_id