package fstar

You can search for identifiers within the package.

in-package search v0.2.0

package fstar

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type pattern = Prims.unit

type eqtype_u = Prims.unit

type !'p spinoff = 'p

val id : 'a -> 'a

type ('a, 'uuuuu) trivial_pure_post = Prims.unit

type ('uuuuu, 'uuuuu1) ambient = Prims.unit

type ('a, 'x, 'uuuuu) pure_return = Prims.unit

type ('a, 'b, !'wp1, 'wp2, 'uuuuu) pure_bind_wp = 'wp1

type ('a, 'p, 'wputhen, 'wpuelse, 'uuuuu) pure_if_then_else = Prims.unit

type ('a, 'wp, 'uuuuu) pure_ite_wp = Prims.unit

type ('a, 'b, 'wp, 'uuuuu) pure_close_wp = Prims.unit

type ('a, 'uuuuu) pure_null_wp = Prims.unit

type ('p, 'uuuuu) pure_assert_wp = Prims.unit

type ('p, 'uuuuu) pure_assume_wp = Prims.unit

type ('a, 'pre, 'post, 'uuuuu) div_hoare_to_wp = Prims.unit

type 'heap st_pre_h = Prims.unit

type ('heap, 'a, 'pre) st_post_h' = Prims.unit

type ('heap, 'a) st_post_h = Prims.unit

type ('heap, 'a) st_wp_h = Prims.unit

type ('heap, 'a, 'x, !'p, 'uuuuu) st_return = 'p

type ('heap, 'a, 'b, !'wp1, 'wp2, 'p, 'h0) st_bind_wp = 'wp1

type ('heap, 'a, 'p, 'wputhen, 'wpuelse, 'post, 'h0) st_if_then_else =
  Prims.unit

type ('heap, 'a, 'wp, 'post, 'h0) st_ite_wp = Prims.unit

type ('heap, 'a, 'wp1, 'wp2) st_stronger = Prims.unit

type ('heap, 'a, 'b, 'wp, 'p, 'h) st_close_wp = Prims.unit

type ('heap, 'a, 'wp) st_trivial = Prims.unit

type !'a result =

| V of 'a
| E of Prims.exn
| Err of Prims.string

val uu___is_V : 'a result -> Prims.bool

val __proj__V__item__v : 'a result -> 'a

val uu___is_E : 'a result -> Prims.bool

val __proj__E__item__e : 'a result -> Prims.exn

val uu___is_Err : 'a result -> Prims.bool

val __proj__Err__item__msg : 'a result -> Prims.string

type ex_pre = Prims.unit

type ('a, 'pre) ex_post' = Prims.unit

type 'a ex_post = Prims.unit

type 'a ex_wp = Prims.unit

type ('a, 'x, !'p) ex_return = 'p

type ('a, 'b, 'wp1, 'wp2, 'p) ex_bind_wp = Prims.unit

type ('a, 'p, 'wputhen, 'wpuelse, 'post) ex_if_then_else = Prims.unit

type ('a, 'wp, 'post) ex_ite_wp = Prims.unit

type ('a, 'wp1, 'wp2) ex_stronger = Prims.unit

type ('a, 'b, 'wp, 'p) ex_close_wp = Prims.unit

type ('a, !'wp) ex_trivial = 'wp

type ('a, !'wp, 'p) lift_div_exn = 'wp

type 'h all_pre_h = Prims.unit

type ('h, 'a, 'pre) all_post_h' = Prims.unit

type ('h, 'a) all_post_h = Prims.unit

type ('h, 'a) all_wp_h = Prims.unit

type ('heap, 'a, 'x, !'p, 'uuuuu) all_return = 'p

type ('heap, 'a, 'b, !'wp1, 'wp2, 'p, 'h0) all_bind_wp = 'wp1

type ('heap, 'a, 'p, 'wputhen, 'wpuelse, 'post, 'h0) all_if_then_else =
  Prims.unit

type ('heap, 'a, 'wp, 'post, 'h0) all_ite_wp = Prims.unit

type ('heap, 'a, 'wp1, 'wp2) all_stronger = Prims.unit

type ('heap, 'a, 'b, 'wp, 'p, 'h) all_close_wp = Prims.unit

type ('heap, 'a, 'wp) all_trivial = Prims.unit

type 'uuuuu inversion = Prims.unit

type (!'a, !'b) either =

| Inl of 'a
| Inr of 'b

val uu___is_Inl : ('a, 'b) either -> Prims.bool

val __proj__Inl__item__v : ('a, 'b) either -> 'a

val uu___is_Inr : ('a, 'b) either -> Prims.bool

val __proj__Inr__item__v : ('a, 'b) either -> 'b

val dfst : ('a, 'b) Prims.dtuple2 -> 'a

val dsnd : ('a, 'b) Prims.dtuple2 -> 'b

type (!'a, !'b, !'c) dtuple3 =

| Mkdtuple3 of 'a * 'b * 'c

val uu___is_Mkdtuple3 : ('a, 'b, 'c) dtuple3 -> Prims.bool

val __proj__Mkdtuple3__item___1 : ('a, 'b, 'c) dtuple3 -> 'a

val __proj__Mkdtuple3__item___2 : ('a, 'b, 'c) dtuple3 -> 'b

val __proj__Mkdtuple3__item___3 : ('a, 'b, 'c) dtuple3 -> 'c

type (!'a, !'b, !'c, !'d) dtuple4 =

| Mkdtuple4 of 'a * 'b * 'c * 'd

val uu___is_Mkdtuple4 : ('a, 'b, 'c, 'd) dtuple4 -> Prims.bool

val __proj__Mkdtuple4__item___1 : ('a, 'b, 'c, 'd) dtuple4 -> 'a

val __proj__Mkdtuple4__item___2 : ('a, 'b, 'c, 'd) dtuple4 -> 'b

val __proj__Mkdtuple4__item___3 : ('a, 'b, 'c, 'd) dtuple4 -> 'c

val __proj__Mkdtuple4__item___4 : ('a, 'b, 'c, 'd) dtuple4 -> 'd

type (!'a, !'b, !'c, !'d, !'e) dtuple5 =

| Mkdtuple5 of 'a * 'b * 'c * 'd * 'e

val uu___is_Mkdtuple5 : ('a, 'b, 'c, 'd, 'e) dtuple5 -> Prims.bool

val __proj__Mkdtuple5__item___1 : ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'a

val __proj__Mkdtuple5__item___2 : ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'b

val __proj__Mkdtuple5__item___3 : ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'c

val __proj__Mkdtuple5__item___4 : ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'd

val __proj__Mkdtuple5__item___5 : ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'e

val false_elim : Prims.unit -> 'uuuuu

val singleton : 'uuuuu -> 'uuuuu

type !'a eqtype_as_type = 'a

val coerce_eq : Prims.unit -> 'a -> 'b