let fractional (a:Type u#a) = option (a & perm)
let fractional (a: Type u#a) =
option (a & perm)
Steel.PCMFrac.fst.checked
Steel.FractionalPermission.fst.checked prims.fst.checked FStar.Real.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PCM.fst.checked FStar.Ghost.fsti.checked
Steel.PCMFrac.fst
FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Steel.FractionalPermission.perm
module Steel.PCMFrac
include FStar.PCM
include Steel.FractionalPermission
open FStar.Real
val fractional : a: Type -> Type
a: Type -> Type