val empty_borrows (#a: _) : borrows a
val empty_borrows (#a: _) : borrows a
let empty_borrows #a
  : borrows a
  = PartialMap.empty M.epoch_id a
module Zeta.Steel.EpochMap
open Steel.ST.Util
open Zeta.Steel.Util
module M = Zeta.Steel.ThreadStateModel
module G = FStar.Ghost
module Set = FStar.Set
module Map = FStar.Map
module U32 = FStar.UInt32

val tbl (#v:Type0)
        (#c:Type0) 
        (vp:M.epoch_id -> v -> c -> vprop)
    : Type0

let repr (a:Type)
  : Type0
  = m:Map.t M.epoch_id a {
      Map.domain m `Set.equal` Set.complement Set.empty
    }

let borrows (a:Type)
  : Type0
  = FStar.PartialMap.t M.epoch_id a
/
Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Steel.ST.Util.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Map.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.EpochMap.fsti
Zeta.Steel.EpochMap.borrows a
FStar.PartialMap.empty Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.EpochMap.borrows
let empty_borrows #a : borrows a =
  
PartialMap.empty M.epoch_id a