fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type aloc_t = Prims.unit
val uu___is_Cls : 'aloc cls -> Prims.bool
type (!'al, !'c) aloc =
  1. | ALoc of Prims.unit * Prims.nat * 'al FStar_Pervasives_Native.option
val uu___is_ALoc : 'al cls -> ('al, Prims.unit) aloc -> Prims.bool
val __proj__ALoc__item__addr : 'al cls -> ('al, Prims.unit) aloc -> Prims.nat
val __proj__ALoc__item__loc : 'al cls -> ('al, Prims.unit) aloc -> 'al FStar_Pervasives_Native.option
type ('a, 'b) i_restricted_g_t = Prims.unit
type 'regions addrs_dom = Prims.unit
type ('regions, 'regionulivenessutags, 'r) non_live_addrs_codom = Prims.unit
type ('regions, 'regionulivenessutags, 'nonuliveuaddrs, 'r) live_addrs_codom = Prims.unit
type (!'al, !'c) loc' =
  1. | Loc of Prims.unit * Prims.unit * Prims.unit * Prims.unit * Prims.unit
val uu___is_Loc : 'al cls -> ('al, Prims.unit) loc' -> Prims.bool
type (!'aloc1, 'c) loc = ('aloc1, Prims.unit) loc'
val loc_none : 'a cls -> ('a, Prims.unit) loc'
type ('t, 'tu, 'p, 'f1, 'f2) fun_set_equal = Prims.unit
type ('al, 'c, 's1, 's2) loc_equal = Obj.t
type ('al, 'c, 'b0, 'b) aloc_includes = Prims.unit
type ('al, 'c, 's, 'b) loc_aux_includes_buffer = Prims.unit
type ('al, 'c, 's1, 's2) loc_aux_includes = Prims.unit
type ('al, 'c, 's1, 's2) loc_includes' = Prims.unit
type ('al, 'c, 's1, 's2) loc_includes = Prims.unit
type ('al, 'c, 'b1, 'b2) aloc_disjoint = Obj.t
type ('al, 'c, 'l1, 'l2) loc_aux_disjoint = Prims.unit
type ('al, 'c, 'l1, 'l2) loc_disjoint_region_liveness_tags = Prims.unit
type ('al, 'c, 'l1, 'l2) loc_disjoint_addrs = Prims.unit
type ('al, 'c, 'l1, 'l2) loc_disjoint_aux = Prims.unit
type ('al, 'c, 'l1, 'l2) loc_disjoint' = Prims.unit
type ('aloc1, 'c, 's1, 's2) loc_disjoint = Prims.unit
val address_liveness_insensitive_locs : 'al cls -> ('al, Prims.unit) loc'
val region_liveness_insensitive_locs : 'al cls -> ('al, Prims.unit) loc'
type ('al, 'c, 's, 'h1, 'h2) modifies_preserves_livenesses = Prims.unit
type ('al, 'c, 's, 'h1, 'h2) modifies_preserves_mreferences = Prims.unit
type ('al, 'c, 's, 'h1, 'h2) modifies_preserves_alocs = Prims.unit
type ('al, 'c, 's, 'h1, 'h2) modifies_preserves_regions = Prims.unit
type ('al, 'c, 's, 'h1, 'h2) modifies_preserves_not_unused_in = Prims.unit
type ('al, 'c, 's, 'h1, 'h2) modifies' = Prims.unit
type ('aloc1, 'c, 's, 'h1, 'h2) modifies = Prims.unit
type ('h, 'ra) does_not_contain_addr' = Prims.unit
type ('h, 'ra) does_not_contain_addr = Prims.unit
type (!'al, !'r, !'n) cls_union_aloc =
  1. | ALOC_FALSE of 'al
  2. | ALOC_TRUE of 'al
val uu___is_ALOC_FALSE : Prims.unit -> Prims.nat -> ('al, Prims.unit, Prims.unit) cls_union_aloc -> Prims.bool
val __proj__ALOC_FALSE__item___0 : Prims.unit -> Prims.nat -> ('al, Prims.unit, Prims.unit) cls_union_aloc -> 'al
val uu___is_ALOC_TRUE : Prims.unit -> Prims.nat -> ('al, Prims.unit, Prims.unit) cls_union_aloc -> Prims.bool
val __proj__ALOC_TRUE__item___0 : Prims.unit -> Prims.nat -> ('al, Prims.unit, Prims.unit) cls_union_aloc -> 'al
val bool_of_cls_union_aloc : Prims.unit -> Prims.nat -> ('al, Prims.unit, Prims.unit) cls_union_aloc -> Prims.bool
val aloc_of_cls_union_aloc : Prims.unit -> Prims.nat -> ('al, Prims.unit, Prims.unit) cls_union_aloc -> 'al
val make_cls_union_aloc : Prims.bool -> Prims.unit -> Prims.nat -> 'al -> ('al, Prims.unit, Prims.unit) cls_union_aloc
type ('al, 'c, 'r, 'a, 'larger, 'smaller) cls_union_aloc_includes = Prims.unit
type ('al, 'c, 'r, 'a, 'larger, 'smaller) cls_union_aloc_disjoint = Prims.unit
type ('al, 'c, 'r, 'a, 'x, 'h, 'hu) cls_union_aloc_preserved = Obj.t
type (!'uuuuu, 'uuuuu1, 'uuuuu2) aloc_union = ('uuuuu, Prims.unit, Prims.unit) cls_union_aloc
val cls_union : (Prims.bool -> 'al cls) -> ('al, Prims.unit, Prims.unit) cls_union_aloc cls
type (!'al, 'r, 'n) raise_aloc = 'al FStar_Universe.raise_t
val raise_cls : 'al cls -> 'al FStar_Universe.raise_t cls
val downgrade_aloc : 'al cls -> ('al FStar_Universe.raise_t, Prims.unit) aloc -> ('al, Prims.unit) aloc
val upgrade_aloc : 'al cls -> ('al, Prims.unit) aloc -> ('al FStar_Universe.raise_t, Prims.unit) aloc
val raise_loc : 'al cls -> ('al, Prims.unit) loc' -> ('al FStar_Universe.raise_t, Prims.unit) loc'
val lower_loc : 'al cls -> ('al FStar_Universe.raise_t, Prims.unit) loc' -> ('al, Prims.unit) loc'