package fstar

  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ('a, 'b) fact1 = Prims.unit
type ('a, 'b) fact0 = Prims.unit
val constant_time_carry : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt64.t
type uint128 = {
  1. low : FStar_UInt64.t;
  2. high : FStar_UInt64.t;
}
val __proj__Mkuint128__item__low : uint128 -> FStar_UInt64.t
val __proj__Mkuint128__item__high : uint128 -> FStar_UInt64.t
type t = uint128
val uint_to_t : Prims.unit FStar_UInt.uint_t -> t
val add : t -> t -> t
val add_underspec : t -> t -> t
val add_mod : t -> t -> t
val sub : t -> t -> t
val sub_underspec : t -> t -> t
val sub_mod_impl : t -> t -> t
val sub_mod : t -> t -> t
val logand : t -> t -> t
val logxor : t -> t -> t
val logor : t -> t -> t
val lognot : t -> t
val __uint_to_t : Prims.int -> t
val u32_64 : FStar_UInt32.t
val add_u64_shift_left_respec : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t
val shift_left_small : t -> FStar_UInt32.t -> t
val shift_left_large : t -> FStar_UInt32.t -> t
val shift_left : t -> FStar_UInt32.t -> t
val add_u64_shift_right : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t
val add_u64_shift_right_respec : FStar_UInt64.t -> FStar_UInt64.t -> FStar_UInt32.t -> FStar_UInt64.t
val shift_right_small : t -> FStar_UInt32.t -> t
val shift_right_large : t -> FStar_UInt32.t -> t
val shift_right : t -> FStar_UInt32.t -> t
val eq : t -> t -> Prims.bool
val gt : t -> t -> Prims.bool
val lt : t -> t -> Prims.bool
val gte : t -> t -> Prims.bool
val lte : t -> t -> Prims.bool
val eq_mask : t -> t -> t
val gte_mask : t -> t -> t
val uint64_to_uint128 : FStar_UInt64.t -> t
val uint128_to_uint64 : t -> FStar_UInt64.t
val u64_l32_mask : FStar_UInt64.t
val u64_mod_32 : FStar_UInt64.t -> FStar_UInt64.t
val u32_32 : FStar_UInt32.t
val mul32 : FStar_UInt64.t -> FStar_UInt32.t -> t
val mul_wide_low : FStar_UInt64.t -> FStar_UInt64.t -> Prims.int
val mul_wide_high : FStar_UInt64.t -> FStar_UInt64.t -> Prims.int
val mul_wide : FStar_UInt64.t -> FStar_UInt64.t -> t
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