val compose (#a: _) (f0: fractional a) (f1: fractional a {composable f0 f1}) : fractional a
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 compose (#a: _) (f0: fractional a) (f1: fractional a {composable f0 f1}) : fractional a
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)
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
Steel.PCMFrac.fractional Steel.PCMFrac.composable FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Steel.FractionalPermission.perm FStar.Pervasives.Native.Some Steel.FractionalPermission.sum_perm
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
val compose (#a: _) (f0: fractional a) (f1: fractional a {composable f0 f1}) : fractional a
f0: Steel.PCMFrac.fractional a -> f1: Steel.PCMFrac.fractional a {Steel.PCMFrac.composable f0 f1}
  -> Steel.PCMFrac.fractional a