val composable (#a: _) : symrel (fractional a)
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 composable (#a: _) : symrel (fractional a)
let composable #a : symrel (fractional a) =
fun (f0: fractional a) (f1: fractional a) ->
  match f0, f1 with
  | None, _ | _, None -> True
  | Some (x0, p0), Some (x1, p1) -> x0 == x1 /\ (sum_perm p0 p1).v <=. one
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 FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 Steel.FractionalPermission.perm Prims.l_True Prims.l_and Prims.eq2 Prims.b2t FStar.Real.op_Less_Equals_Dot Steel.FractionalPermission.__proj__MkPerm__item__v Steel.FractionalPermission.sum_perm FStar.Real.one Prims.prop FStar.PCM.symrel
module Steel.PCMFrac
include FStar.PCM
include Steel.FractionalPermission
open FStar.Real

let fractional (a:Type u#a) = option (a & perm)
val composable (#a: _) : symrel (fractional a)
FStar.PCM.symrel (Steel.PCMFrac.fractional a)