fstar
  1. Overview
  2. Docs
package fstar
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'n swap = Prims.nat
val apply_swap_aux : Prims.nat -> 'a Prims.list -> Prims.nat -> 'a Prims.list
val apply_swap : Prims.unit -> 'a Prims.list -> Prims.nat -> 'a Prims.list
val apply_swaps : 'a Prims.list -> Prims.nat Prims.list -> 'a Prims.list
type ('a, 'xs, 'ys) equal_counts = Prims.unit
type ('a, 'xs) swap_for = Prims.unit swap
type ('a, 'xs) swaps_for = Prims.unit swap Prims.list
val lift_swaps_cons : 'a -> 'a Prims.list -> Prims.nat Prims.list -> Prims.nat Prims.list
val swap_to_front : 'a -> 'a Prims.list -> Prims.nat Prims.list
val equal_counts_implies_swaps : 'a Prims.list -> 'a Prims.list -> Prims.nat Prims.list