val pcm_frac (#a: _) : pcm (fractional a)
let pcm_frac #a : pcm (fractional a) = {
  p = {
         composable = composable;
         op = compose;
         one = None
      };
  comm = (fun _ _ -> ());
  assoc = (fun _ _ _ -> ());
  assoc_r = (fun _ _ _ -> ());
  is_unit = (fun _ -> ());
  refine = (fun _ -> True)
}
val pcm_frac (#a: _) : pcm (fractional a)
let pcm_frac #a : pcm (fractional a) =
{
  p = { composable = composable; op = compose; one = None };
  comm = (fun _ _ -> ());
  assoc = (fun _ _ _ -> ());
  assoc_r = (fun _ _ _ -> ());
  is_unit = (fun _ -> ());
  refine = (fun _ -> True)
}
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.PCM.Mkpcm Steel.PCMFrac.fractional FStar.PCM.Mkpcm' Steel.PCMFrac.composable Steel.PCMFrac.compose FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 Steel.FractionalPermission.perm FStar.PCM.__proj__Mkpcm'__item__composable Prims.unit Prims.l_and FStar.PCM.__proj__Mkpcm'__item__op Prims.l_True Prims.prop FStar.PCM.pcm
module Steel.PCMFrac
include FStar.PCM
include Steel.FractionalPermission
open FStar.Real

let fractional (a:Type u#a) = option (a & perm)
let composable #a : symrel (fractional a) =
  fun (f0 f1:fractional a) ->
    match f0, f1 with
    | None, _
    | _, None -> True
    | Some (x0, p0), Some (x1, p1) -> x0==x1 /\ (sum_perm p0 p1).v <=. one
let compose #a (f0:fractional a) (f1:fractional a{composable f0 f1}) : fractional a =
  match f0, f1 with
  | None, f
  | f, None -> f
  | Some (x0, p0), Some (_, p1) -> Some (x0, sum_perm p0 p1)
val pcm_frac (#a: _) : pcm (fractional a)
FStar.PCM.pcm (Steel.PCMFrac.fractional a)