package fstar

  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type int = Z.t
val of_int : int -> Z.t
val int_zero : Z.t
val int_one : Z.t
val parse_int : string -> Z.t
val to_string : Z.t -> string
type tmp = string
val tmp_to_yojson : tmp -> Yojson.Safe.t
val int_to_yojson : Z.t -> Yojson.Safe.t
val int_of_yojson : Yojson.Safe.t -> (Z.t, string) result
type attribute = unit
val cps : attribute
type 'Auu____5 hasEq = unit
type eqtype = unit
type bool' = bool
val bool'_to_yojson : bool' -> Yojson.Safe.t
type bool = bool'
val bool_to_yojson : bool -> Yojson.Safe.t
type empty = unit
type trivial =
  1. | T
val uu___is_T : trivial -> bool
type nonrec unit = unit
type 'Ap squash = unit
type 'Ap auto_squash = unit
type l_True = unit
type l_False = unit
type (!'Aa, !'Ax, !'dummyV0) equals =
  1. | Refl
val uu___is_Refl : 'Aa -> 'Aa -> ('Aa, unit, unit) equals -> bool
type ('Aa, 'Ax, 'Ay) eq2 = unit
type ('Aa, 'Ab, 'Ax, 'Ay) op_Equals_Equals_Equals = unit
type 'Ab b2t = unit
type (!'Ap, !'Aq) pair =
  1. | Pair of 'Ap * 'Aq
val uu___is_Pair : ('Ap, 'Aq) pair -> bool
val __proj__Pair__item___1 : ('Ap, 'Aq) pair -> 'Ap
val __proj__Pair__item___2 : ('Ap, 'Aq) pair -> 'Aq
type ('Ap, 'Aq) l_and = unit
type (!'Ap, !'Aq) sum =
  1. | Left of 'Ap
  2. | Right of 'Aq
val uu___is_Left : ('Ap, 'Aq) sum -> bool
val __proj__Left__item___0 : ('Ap, 'Aq) sum -> 'Ap
val uu___is_Right : ('Ap, 'Aq) sum -> bool
val __proj__Right__item___0 : ('Ap, 'Aq) sum -> 'Aq
type ('Ap, 'Aq) l_or = unit
type ('Ap, 'Aq) l_imp = unit
type ('Ap, 'Aq) l_iff = unit
type 'Ap l_not = unit
type ('Ap, 'Aq, 'Ar) l_ITE = unit
type ('Aa, 'Ab, 'Auu____484, 'Auu____485) precedes = unit
type ('Aa, 'Auu____490, 'Auu____491) has_type = unit
type ('Aa, 'Ap) l_Forall = unit
type prop = unit
val id : 'a -> 'a
type (!'Aa, !'Ab) dtuple2 =
  1. | Mkdtuple2 of 'Aa * 'Ab
val uu___is_Mkdtuple2 : ('Aa, 'Ab) dtuple2 -> bool
val __proj__Mkdtuple2__item___1 : ('Aa, 'Ab) dtuple2 -> 'Aa
val __proj__Mkdtuple2__item___2 : ('Aa, 'Ab) dtuple2 -> 'Ab
type ('Aa, 'Ap) l_Exists = unit
type string' = string
val string'_to_yojson : string' -> Yojson.Safe.t
val show_string' : string' -> Ppx_deriving_runtime.string
type string = string'
val string_to_yojson : string -> Yojson.Safe.t
val show_string : string -> Ppx_deriving_runtime.string
type pure_pre = unit
type ('Aa, 'Apre) pure_post' = unit
type 'Aa pure_post = unit
type 'Aa pure_wp = unit
type 'Auu____655 guard_free = unit
type ('Aa, 'Ax, 'Ap) pure_return = unit
type ('Ar1, 'Aa, 'Ab, !'Awp1, 'Awp2, 'Ap) pure_bind_wp = 'Awp1
type ('Aa, 'Ap, 'Awp_then, 'Awp_else, 'Apost) pure_if_then_else = unit
val pure_if_then_else_to_yojson : ('Aa -> Yojson.Safe.t) -> ('Ap -> Yojson.Safe.t) -> ('Awp_then -> Yojson.Safe.t) -> ('Awp_else -> Yojson.Safe.t) -> ('Apost -> Yojson.Safe.t) -> ('Aa, 'Ap, 'Awp_then, 'Awp_else, 'Apost) pure_if_then_else -> Yojson.Safe.t
type ('Aa, 'Awp, 'Apost) pure_ite_wp = unit
type ('Aa, 'Awp1, 'Awp2) pure_stronger = unit
type ('Aa, 'Ab, 'Awp, 'Ap) pure_close_wp = unit
type ('Aa, 'Aq, 'Awp, 'Ap) pure_assert_p = unit
type ('Aa, 'Aq, 'Awp, 'Ap) pure_assume_p = unit
type ('Aa, 'Ap) pure_null_wp = unit
type ('Aa, !'Awp) pure_trivial = 'Awp
type ('Ap, 'Apost) pure_assert_wp = unit
type ('Aa, !'Awp, 'Auu____878) purewp_id = 'Awp
val op_AmpAmp : bool -> bool -> bool
val op_BarBar : bool -> bool -> bool
val op_Negation : bool -> bool
val (+) : Z.t -> Z.t -> Z.t
val (-) : Z.t -> Z.t -> Z.t
val (*) : Z.t -> Z.t -> Z.t
val (/) : Z.t -> Z.t -> Z.t
val (<=) : Z.t -> Z.t -> bool
val (>=) : Z.t -> Z.t -> bool
val (<) : Z.t -> Z.t -> bool
val (>) : Z.t -> Z.t -> bool
val (mod) : Z.t -> Z.t -> Z.t
val (~-) : Z.t -> Z.t
val op_Multiply : Z.t -> Z.t -> Z.t
val op_Subtraction : Z.t -> Z.t -> Z.t
val op_Addition : Z.t -> Z.t -> Z.t
val op_Minus : Z.t -> Z.t
val op_LessThan : Z.t -> Z.t -> bool
val op_LessThanOrEqual : Z.t -> Z.t -> bool
val op_GreaterThan : Z.t -> Z.t -> bool
val op_GreaterThanOrEqual : Z.t -> Z.t -> bool
val op_Equality : 'a -> 'a -> bool
val op_disEquality : 'a -> 'a -> bool
type nonrec exn = exn
type !'a array' = 'a array
val array'_to_yojson : ('a -> Yojson.Safe.t) -> 'a array' -> Yojson.Safe.t
type !'a array = 'a array'
val array_to_yojson : ('a -> Yojson.Safe.t) -> 'a array -> Yojson.Safe.t
val strcat : string -> string -> string
val op_Hat : string -> string -> string
type !'a list' = 'a list
val list'_to_yojson : ('a -> Yojson.Safe.t) -> 'a list' -> Yojson.Safe.t
type !'a list = 'a list'
val list_to_yojson : ('a -> Yojson.Safe.t) -> 'a list -> Yojson.Safe.t
val _ : (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) -> Yojson.Safe.t -> 'a list Ppx_deriving_yojson_runtime.error_or
val uu___is_Nil : 'Aa list -> bool
val uu___is_Cons : 'Aa list -> bool
val __proj__Cons__item__hd : 'Aa list -> 'Aa
val __proj__Cons__item__tl : 'Aa list -> 'Aa list
type pattern = unit
type ('Aa, 'Auu____1278) decreases = unit
val returnM : 'Aa -> 'Aa
type lex_t =
  1. | LexTop
  2. | LexCons of unit * Obj.t * lex_t
val uu___is_LexTop : lex_t -> bool
val uu___is_LexCons : lex_t -> bool
type 'Aprojectee __proj__LexCons__item__a = Obj.t
val __proj__LexCons__item___1 : lex_t -> Obj.t
val __proj__LexCons__item___2 : lex_t -> lex_t
type ('Aa, !'Awp) as_requires = 'Awp
type ('Aa, 'Awp, 'Ax) as_ensures = unit
val admit : unit -> 'a
val magic : unit -> 'a
val unsafe_coerce : 'Aa -> 'Ab
type !'Ap spinoff = 'Ap
type nat = int
type pos = int
type nonzero = int
val op_Modulus : Z.t -> Z.t -> Z.t
val op_Division : Z.t -> Z.t -> Z.t
val pow2 : nat -> pos
val min : int -> int -> int
val abs : int -> int
val string_of_bool : bool -> string
val string_of_int : Z.t -> string
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct