val typeof (#t: Type0) (td: typedef t) : Tot Type0
let typeof (#t: Type0) (td: typedef t) : Tot Type0 = t
val typeof (#t: Type0) (td: typedef t) : Tot Type0
let typeof (#t: Type0) (td: typedef t) : Tot Type0 =
t
Steel.ST.C.Types.Base.fsti.checked
Steel.ST.Util.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.StrongExcludedMiddle.fst.checked FStar.Real.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.C.Types.Base.fsti
Steel.ST.C.Types.Base.typedef
module Steel.ST.C.Types.Base
open Steel.ST.Util

module P = Steel.FractionalPermission

/// Helper to compose two permissions into one
val prod_perm (p1 p2: P.perm) : Pure P.perm
  (requires True)
  (ensures (fun p ->
    ((p1 `P.lesser_equal_perm` P.full_perm /\ p2 `P.lesser_equal_perm` P.full_perm) ==>
    p `P.lesser_equal_perm` P.full_perm) /\
    p.v == (let open FStar.Real in p1.v *. p2.v)
  ))

[@@noextract_to "krml"] // proof-only
val typedef (t: Type0) : Type0
val typeof (#t: Type0) (td: typedef t) : Tot Type0
td: Steel.ST.C.Types.Base.typedef t -> Type0