val mk_frame_preserving_upd (#a: Type) (v0: Ghost.erased a) (v1: a)
    : Tot (frame_preserving_upd pcm_frac (Some (Ghost.reveal v0, full_perm)) (Some (v1, full_perm)))
let mk_frame_preserving_upd
  (#a: Type)
  (v0: Ghost.erased a)
  (v1: a)
: Tot (frame_preserving_upd pcm_frac (Some (Ghost.reveal v0, full_perm)) (Some (v1, full_perm)))
= fun _ -> Some (v1, full_perm)
val mk_frame_preserving_upd (#a: Type) (v0: Ghost.erased a) (v1: a)
    : Tot (frame_preserving_upd pcm_frac (Some (Ghost.reveal v0, full_perm)) (Some (v1, full_perm)))
let mk_frame_preserving_upd (#a: Type) (v0: Ghost.erased a) (v1: a)
    : Tot (frame_preserving_upd pcm_frac (Some (Ghost.reveal v0, full_perm)) (Some (v1, full_perm))) =
fun _ -> Some (v1, full_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.Ghost.erased Steel.PCMFrac.fractional Prims.l_and FStar.PCM.__proj__Mkpcm__item__refine Steel.PCMFrac.pcm_frac FStar.PCM.compatible FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 Steel.FractionalPermission.perm FStar.Pervasives.Native.Mktuple2 FStar.Ghost.reveal Steel.FractionalPermission.full_perm Prims.l_Forall FStar.PCM.composable Prims.l_imp Prims.eq2 FStar.PCM.op FStar.PCM.frame_preserving_upd
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)

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)
}

let mk_frame_preserving_upd
  (#a: Type)
  (v0: Ghost.erased a)
  (v1: a)
val mk_frame_preserving_upd (#a: Type) (v0: Ghost.erased a) (v1: a)
    : Tot (frame_preserving_upd pcm_frac (Some (Ghost.reveal v0, full_perm)) (Some (v1, full_perm)))
v0: FStar.Ghost.erased a -> v1: a
  -> FStar.PCM.frame_preserving_upd Steel.PCMFrac.pcm_frac
      (FStar.Pervasives.Native.Some (FStar.Ghost.reveal v0, Steel.FractionalPermission.full_perm))
      (FStar.Pervasives.Native.Some (v1, Steel.FractionalPermission.full_perm))