val half : Steel.FractionalPermission.perm
let half = Steel.FractionalPermission.half_perm full
module Zeta.Steel.Util
open Steel.ST.Util
module A = Steel.ST.Array
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module Cast = FStar.Int.Cast
/
Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.fst.checked
Zeta.Steel.Util.fst
Steel.FractionalPermission.perm
Steel.FractionalPermission.half_perm Zeta.Steel.Util.full
let half =
  
Steel.FractionalPermission.half_perm full