fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type ('a, 's1, 's2) grows_aux = Prims.unit
type ('a, 'uuuuu, 'uuuuu1) grows = Prims.unit
type rid = Prims.unit
val snoc : 'a FStar_Seq_Base.seq -> 'a -> 'a FStar_Seq_Base.seq
type ('a, 'i, 'n, 'x, 'r, 'h) at_least = Prims.unit
type ('a, 'p, 's1, 's2) grows_p = Prims.unit
type ('r, 'a, 'p, 'n, 'x, 'm, 'h) i_at_least = Prims.unit
type ('r, 'a, 'p, 'x, 'is, 'h) int_at_most = Prims.unit
type ('r, 'a, 'p, 'm, 'h) i_contains = Prims.unit
type 's invariant = Prims.unit
val un_snoc : 'a FStar_Seq_Base.seq -> 'a FStar_Seq_Base.seq * 'a
val map : ('a -> 'b) -> 'a FStar_Seq_Base.seq -> 'b FStar_Seq_Base.seq
val op_At : 'uuuuu FStar_Seq_Base.seq -> 'uuuuu FStar_Seq_Base.seq -> 'uuuuu FStar_Seq_Base.seq
type ('a, 'b, 'i, 'r, 'f, 'bs, 'h) map_prefix = Prims.unit
type ('a, 'b, 'i, 'r, 'f, 'n, 'v, 'h) map_has_at_index = Prims.unit
val collect : ('a -> 'b FStar_Seq_Base.seq) -> 'a FStar_Seq_Base.seq -> 'b FStar_Seq_Base.seq
type ('a, 'b, 'i, 'r, 'f, 'bs, 'h) collect_prefix = Prims.unit
type ('a, 'b, 'i, 'r, 'f, 'n, 'v, 'h) collect_has_at_index = Prims.unit
type ('x, 'y) increases = Prims.unit
type ('l, 'a, 'x, 'log, 'h) at_most_log_len = Prims.unit
type ('l, 'a, 'i, 'log, 'max) seqn_val = Prims.nat