package fstar

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

val disjoint_only_lemma : 'a -> 'b -> 'c -> 'd -> unit

val eq_lemma : 'a -> 'b -> 'c -> 'd -> 'e -> unit

val modifies_transitivity_lemma : 'a -> 'b -> 'c -> 'd -> unit

val modifies_subset_lemma : 'a -> 'b -> 'c -> 'd -> unit

val modifies_empty_lemma : 'a -> unit

val modifies_fresh_lemma : 'a -> 'b -> 'c -> 'd -> 'e -> unit

type ('a, 'b, 'c, 'd) disjoint = unit

type ('a, 'b, 'c) live = unit

type abuffer =

type !'a buffer = {

}

type u8 = FStar_UInt8.t

type u32 = FStar_UInt32.t

type u64 = FStar_UInt64.t

type u128 = FStar_UInt128.t

type uint8s = u8 buffer

type uint32s = u32 buffer

type uint64s = u64 buffer

type uint128s = u128 buffer

val create : 'a -> int -> 'a buffer

val createL : 'a list -> 'a buffer

val rcreate : 'a -> 'b -> int -> 'b buffer

val index : 'a buffer -> int -> 'a

val upd : 'a buffer -> u32 -> 'a -> unit

val sub : 'a buffer -> int -> int -> 'a buffer

val offset : 'a buffer -> int -> 'a buffer

val blit : 
  'a buffer ->
  FStar_UInt32.t ->
  'a buffer ->
  FStar_UInt32.t ->
  FStar_UInt32.t ->
  unit

val fill : 'a buffer -> 'a -> FStar_UInt32.t -> unit

val split : 'a buffer -> int -> 'a buffer * 'a buffer

val of_seq : 'a -> 'b -> unit

val copy : 'a buffer -> int -> 'a buffer

val eqb : 'a buffer -> 'a buffer -> u32 -> bool

type ('a, 'b, 'c, 'd) modifies_buf = unit

val op_Plus_Plus : 'a -> 'b -> 'c BatSet.t

val only : 'a -> 'b BatSet.t

val op_Array_Access : 'a buffer -> int -> 'a

val op_Array_Assignment : 'a buffer -> u32 -> 'a -> unit

val recall : 'a -> unit

val of_ocaml_array : 'a array -> 'a buffer

val to_seq_full : 'a -> 'b