val compute_gen_elim_f_unit (i: gen_unit_elim_i) : GTot (gen_elim_t (GEUnit i))
let compute_gen_elim_f_unit
  (i: gen_unit_elim_i)
: GTot (gen_elim_t (GEUnit i))
= compute_gen_unit_elim_f i
val compute_gen_elim_f_unit (i: gen_unit_elim_i) : GTot (gen_elim_t (GEUnit i))
let compute_gen_elim_f_unit (i: gen_unit_elim_i) : GTot (gen_elim_t (GEUnit i)) =
compute_gen_unit_elim_f i
Steel.ST.GenElim.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.GenElim.fst
Steel.ST.GenElim.Base.gen_unit_elim_i Steel.ST.GenElim.compute_gen_unit_elim_f Steel.ST.GenElim.gen_elim_t Steel.ST.GenElim.Base.GEUnit
module Steel.ST.GenElim

let gen_elim_f
  (p: vprop)
  (a: Type0) // FIXME: generalize this universe
  (q: (a -> vprop))
  (post: (a -> prop))
: Tot Type
= ((opened: inames) -> STGhost a opened p q True post)

let gen_unit_elim_t (i: gen_unit_elim_i) : Tot Type =
  gen_elim_f (compute_gen_unit_elim_p i) unit (fun _ -> compute_gen_unit_elim_q i) (fun _ -> compute_gen_unit_elim_post i)

let compute_gen_unit_elim_f_id
  (v: vprop)
: Tot (gen_unit_elim_t (GUEId v))
= fun _ -> noop ()

let compute_gen_unit_elim_f_pure
  (p: prop)
: Tot (gen_unit_elim_t (GUEPure p))
= fun _ ->
  rewrite (compute_gen_unit_elim_p (GUEPure p)) (pure p);
  elim_pure p

let compute_gen_unit_elim_f_star
  (i1 i2: gen_unit_elim_i)
  (f1: gen_unit_elim_t i1)
  (f2: gen_unit_elim_t i2)
: Tot (gen_unit_elim_t (GUEStar i1 i2))
= fun _ ->
  rewrite (compute_gen_unit_elim_p (GUEStar i1 i2)) (compute_gen_unit_elim_p i1 `star` compute_gen_unit_elim_p i2);
  f1 _; f2 _;
  rewrite (compute_gen_unit_elim_q i1 `star` compute_gen_unit_elim_q i2) (compute_gen_unit_elim_q (GUEStar i1 i2))

let rec compute_gen_unit_elim_f
  (i: gen_unit_elim_i)
: GTot (gen_unit_elim_t i)
= match i returns (gen_unit_elim_t i) with
  | GUEId v -> compute_gen_unit_elim_f_id v
  | GUEPure p -> compute_gen_unit_elim_f_pure p
  | GUEStar i1 i2 -> compute_gen_unit_elim_f_star i1 i2 (compute_gen_unit_elim_f i1) (compute_gen_unit_elim_f i2)

let gen_elim_t (i: gen_elim_i) : Tot Type =
  gen_elim_f (compute_gen_elim_p i) (compute_gen_elim_a i) (compute_gen_elim_q i) (compute_gen_elim_post i)

let compute_gen_elim_f_unit
  (i: gen_unit_elim_i)
val compute_gen_elim_f_unit (i: gen_unit_elim_i) : GTot (gen_elim_t (GEUnit i))
i: Steel.ST.GenElim.Base.gen_unit_elim_i
  -> Prims.GTot (Steel.ST.GenElim.gen_elim_t (Steel.ST.GenElim.Base.GEUnit i))