package fstar

You can search for identifiers within the package.

in-package search v0.2.0

fstar.lib

Legend:
Library
Module
Module type
Parameter
Class
Class type

type ('a, 's) index_fun =
  Prims.unit FStar_IntegerIntervals.under ->
  Prims.unit FStar_IntegerIntervals.under

type ('a, 's0, 's1, 'f) is_permutation = Prims.unit

type ('a, 's0, 's1) seqperm = ('a, Prims.unit) index_fun

val find : 
  'a ->
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq * 'a FStar_Seq_Base.seq

val adapt_index_fun : 
  'a FStar_Seq_Base.seq ->
  (Prims.int -> Prims.int) ->
  Prims.nat ->
  Prims.int ->
  Prims.int

val permutation_from_equal_counts : 
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq ->
  Prims.int ->
  Prims.int

val foldm_snoc : 
  'a FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('a, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  'a FStar_Seq_Base.seq ->
  'a

val remove_i : 'a FStar_Seq_Base.seq -> Prims.nat -> 'a * 'a FStar_Seq_Base.seq

val shift_perm' : 
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq ->
  Prims.unit ->
  (Prims.int -> Prims.int) ->
  Prims.int ->
  Prims.int

val shift_perm : 
  'a FStar_Seq_Base.seq ->
  'a FStar_Seq_Base.seq ->
  Prims.unit ->
  (Prims.int -> Prims.int) ->
  Prims.int ->
  Prims.int

val init_func_from_expr : 
  Prims.int ->
  Prims.int ->
  (Prims.int -> 'c) ->
  Prims.int ->
  Prims.int ->
  Prims.int ->
  'c

val func_sum : 
  'c FStar_Algebra_CommMonoid_Equiv.equiv ->
  ('c, Prims.unit) FStar_Algebra_CommMonoid_Equiv.cm ->
  ('a -> 'c) ->
  ('a -> 'c) ->
  'a ->
  'c