module FStar.Universe

fsdoc: no-summary-found

fsdoc: no-comment-found

 This module implements some basic facilities to raise the universe of a type *
  * The type [raise_t a] is supposed to be isomorphic to [a] but in a higher     *
  * universe. The two functions [raise_val] and [dowgrade_val] allow to coerce   *
  * from [a] to [raise_t a] and back.                                            *

val raise_t:Unidentified product: [(Type a)] (Type max a b)

[raise_t a] is an isomorphic copy of [a] (living in universe 'ua) in universe [max 'ua 'ub] *

val raise_val:Unidentified product: [#a:(Type a)] Unidentified product: [x:a] raise_t a b a

[raise_val x] injects a value [x] of type [a] to [raise_t a] *

val downgrade_val:Unidentified product: [#a:(Type a)] Unidentified product: [x:raise_t a b a] a

[downgrade_val x] projects a value [x] of type [raise_t a] to [a] *