Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

argmax

Find the index of the maximum element.

argmin

Find the index of the minimum element.

build_vec_env

Build Vec type in the environment.

flatten_once

Flatten one level of nesting.

group_by

Group consecutive elements by a key function.

indexed_map

Map over a slice and collect the results, also returning the original indices.

is_palindrome

Return true if v is a palindrome.

register_vec_extended_axioms

Register all extended Vec axioms into env.

run_length_decode

Decode a run-length encoded sequence back to a flat vector.

run_length_encode

Run-length encode a slice: consecutive equal elements become (value, count).

same_length_check

Assert that two slices have the same length and return an error otherwise.

vec_append

Concatenate two vectors into a new one.

vec_cartesian_product

Produce all combinations of one element from each inner slice.

vec_chunks

Split a slice into chunks of size.

vec_contains

Return true if v contains elem.

vec_count_where

Count elements matching a predicate.

vec_dedup_stable

Deduplicate a vector (keeping first occurrence), preserving order.

vec_difference

Return elements in a not in b (order-preserving, O(n*m)).

vec_drop

Drop the first n elements.

vec_drop_while

Drop elements while a predicate is true.

vec_ext_build_ap_composition

Vec.ap_composition : ap (ap (ap [∘] fs) gs) xs = ap fs (ap gs xs)

vec_ext_build_ap_homomorphism

Vec.ap_homomorphism : ap [f] [v] = [f v]

vec_ext_build_ap_identity

Vec.ap_identity : ap [id] xs = xs

vec_ext_build_ap_interchange

Vec.ap_interchange : ap fs [v] = ap [fun f => f v] fs

vec_ext_build_append_assoc

Vec.append_assoc : (xs ++ ys) ++ zs = xs ++ (ys ++ zs)

vec_ext_build_append_nil_left

Vec.append_nil_left : [] ++ xs = xs

vec_ext_build_append_nil_right

Vec.append_nil_right : xs ++ [] = xs

vec_ext_build_chunks_all_size

Vec.chunks_all_size : ∀ chunk ∈ init (chunks n xs), length chunk = n

vec_ext_build_chunks_count

Vec.chunks_count : length (chunks n xs) = ceil (length xs / n)

vec_ext_build_chunks_flatten

Vec.chunks_flatten : flatten (chunks n xs) = xs (when n > 0)

vec_ext_build_concat_map_assoc

Vec.concat_map_assoc : concatMap (concatMap f ∘ g) = concatMap f ∘ concatMap g

vec_ext_build_concat_map_id

Vec.concat_map_id : concatMap pure xs = xs

vec_ext_build_dlist_append_assoc

Vec.dlist_append_assoc : dlist append is associative

vec_ext_build_dlist_to_list

Vec.dlist_to_list_preserves : toList (dlist d) = d []

vec_ext_build_drop_length

Vec.drop_length : length (drop n xs) = max 0 (length xs - n)

vec_ext_build_fenwick_correct

Vec.fenwick_prefix_sum_correct : query fenwick i = sum (take (i+1) original)

vec_ext_build_filter_fusion

Vec.filter_fusion : filter p (filter q xs) = filter (fun x => p x && q x) xs

vec_ext_build_fin_index_get

Vec.fin_index_get : ∀ {α n} (xs : Vec α n) (i : Fin n), xs[i] is within bounds

vec_ext_build_fin_index_set

Vec.fin_index_set : ∀ {α n} (xs : Vec α n) (i : Fin n) v, set xs i v has same length

vec_ext_build_fin_map_length

Vec.fin_map_preserves_length : length (map f xs) = length xs

vec_ext_build_flatten_map

Vec.flatten_map : flatten (map (map f) xss) = map f (flatten xss)

vec_ext_build_flatten_singleton

Vec.flatten_singleton : flatten [[x1], [x2], ...] = [x1, x2, ...]

vec_ext_build_fold_build_duality

Vec.fold_build_duality : foldr f z (build g) = g f z (deforestation)

vec_ext_build_foldl_cons

Vec.foldl_cons : foldl f z (x::xs) = foldl f (f z x) xs

vec_ext_build_foldl_foldr_duality

Vec.foldl_foldr_duality : foldl f z xs = foldr (flip f) z (reverse xs)

vec_ext_build_foldl_nil

Vec.foldl_nil : foldl f z [] = z

vec_ext_build_foldr_cons

Vec.foldr_cons : foldr f z (x::xs) = f x (foldr f z xs)

vec_ext_build_foldr_nil

Vec.foldr_nil : foldr f z [] = z

vec_ext_build_functor_map_comp

Vec.functor_map_comp : ∀ α β γ (f : α → β) (g : β → γ), map (g ∘ f) = map g ∘ map f

vec_ext_build_functor_map_id

Vec.functor_map_id : ∀ α, map id xs = xs

vec_ext_build_groupby_flatten

Vec.groupBy_flatten : flatten (groupBy eq xs) = xs

vec_ext_build_length_append

Vec.length_append : length (xs ++ ys) = length xs + length ys

vec_ext_build_map_filter_fusion

Vec.map_filter_fusion : map f (filter p xs) = filterMap (fun x => if p x then Some (f x) else None) xs

vec_ext_build_map_fusion

Vec.map_fusion : map f (map g xs) = map (f ∘ g) xs

vec_ext_build_matrix_col_count

Vec.matrix_col_count : length (head (transpose m)) = length m

vec_ext_build_matrix_row_count

Vec.matrix_row_count : length (transpose m) = length (head m)

vec_ext_build_matrix_transpose_invol

Vec.matrix_transpose_involutive : transpose (transpose m) = m

vec_ext_build_monad_assoc

Vec.monad_assoc : ∀ α β γ, andThen (andThen xs f) g = andThen xs (fun x => andThen (f x) g)

vec_ext_build_monad_left_id

Vec.monad_left_id : ∀ α β (a : α) (f : α → Vec β), andThen [a] f = f a

vec_ext_build_monad_right_id

Vec.monad_right_id : ∀ α (xs : Vec α), andThen xs pure = xs

vec_ext_build_parallel_prefix_equiv

Vec.parallel_prefix_sequential_equiv : parallelPrefix f z xs = scanl f z xs

vec_ext_build_partition_reconstruct

Vec.partition_reconstruct : fst (partition p xs) ++ snd (partition p xs) is permutation

vec_ext_build_prefix_sum_correct

Vec.prefix_sum_correct : prefixSum xs[i] = sum (take (i+1) xs)

vec_ext_build_reverse_append

Vec.reverse_append : reverse (xs ++ ys) = reverse ys ++ reverse xs

vec_ext_build_reverse_involutive

Vec.reverse_involutive : reverse (reverse xs) = xs

vec_ext_build_reverse_map

Vec.reverse_map : reverse (map f xs) = map f (reverse xs)

vec_ext_build_rle_length

Vec.rle_length : sum (map snd (rle xs)) = length xs

vec_ext_build_rle_roundtrip

Vec.rle_decode_encode : decode (encode xs) = xs

vec_ext_build_rotate_left_right_inv

Vec.rotate_left_right_inverse : rotateLeft n (rotateRight n xs) = xs

vec_ext_build_rotate_length

Vec.rotate_length : length (rotateLeft n xs) = length xs

vec_ext_build_rotate_zero

Vec.rotate_zero : rotateLeft 0 xs = xs

vec_ext_build_scanl_cons

Vec.scanl_cons : scanl f z (x::xs) = z :: scanl f (f z x) xs

vec_ext_build_scanl_last

Vec.scanl_last : last (scanl f z xs) = foldl f z xs

vec_ext_build_scanl_nil

Vec.scanl_nil : scanl f z [] = [z]

vec_ext_build_scanr_cons

Vec.scanr_cons : head (scanr f z (x::xs)) = f x (head (scanr f z xs))

vec_ext_build_scanr_nil

Vec.scanr_nil : scanr f z [] = [z]

vec_ext_build_sort_idempotent

Vec.sort_idempotent : sort (sort xs) = sort xs

vec_ext_build_sort_is_permutation

Vec.sort_is_permutation : sort xs is a permutation of xs

vec_ext_build_sort_is_sorted

Vec.sort_is_sorted : ∀ α [Ord α] xs, isSorted (sort xs)

vec_ext_build_span_reconstruct

Vec.span_reconstruct : fst (span p xs) ++ snd (span p xs) = xs

vec_ext_build_stable_sort

Vec.stable_sort_preserves_order : stable sort preserves relative order of equal elements

vec_ext_build_take_drop_reconstruct

Vec.take_drop_reconstruct : take n xs ++ drop n xs = xs

vec_ext_build_take_length

Vec.take_length : length (take n xs) = min n (length xs)

vec_ext_build_unzip_zip

Vec.unzip_zip : unzip (zip xs ys) = (take (min n m) xs, take (min n m) ys)

vec_ext_build_zip_length

Vec.zip_length : length (zip xs ys) = min (length xs) (length ys)

vec_ext_build_zip_map

Vec.zip_map : zip (map f xs) (map g ys) = map (bimap f g) (zip xs ys)

vec_ext_forall1_axiom

Build ∀ (α : Type), Prop.

vec_ext_forall2_axiom

Build ∀ (α β : Type), Prop.

vec_ext_forall3_axiom

Build ∀ (α β γ : Type), Prop.

vec_ext_prop_axiom

vec_flatten

Flatten a Vec<Vec<T>> into a Vec<T>.

vec_head

Return the first element of a slice, or None.

vec_index_of

Return the index of the first occurrence of elem, or None.

vec_init

Return all but the last element (i.e. init of the vector).

vec_insert_at

Insert elem at index, shifting subsequent elements right.

vec_intersection

Return elements in both a and b (order-preserving, keeps first occurrence).

vec_intersperse

Interleave sep between elements of v.

vec_is_subset

Return true if a is a subset of b (all elements of a appear in b).

vec_last

Return the last element of a slice, or None.

vec_max

Return the maximum element of a non-empty slice, or None.

vec_mean_f64

Compute the arithmetic mean of a f64 slice.

vec_median_f64

Compute the median of a f64 slice.

vec_min

Return the minimum element of a non-empty slice, or None.

vec_normalize_f64

Normalise a f64 vector so that its values sum to 1.0.

vec_partition

Partition into matching and non-matching elements.

vec_product_u64

Product of all u64 values in a slice.

vec_remove_all

Remove all occurrences of elem from v.

vec_remove_at

Return the vector with element at index removed.

vec_reverse

Reverse a vector.

vec_rotate_left

Rotate a vector left by n positions.

vec_rotate_right

Rotate a vector right by n positions.

vec_set

Replace the element at index with new_val.

vec_set_eq

Return true if a and b are set-equal (same elements, any order).

vec_split_at

Split a vector at index, returning (left, right).

vec_std_dev_f64

Compute the standard deviation (population) of a f64 slice.

vec_step_by

Return every n-th element starting from start.

vec_sum_u64

Sum all u64 values in a slice.

vec_symmetric_difference

Return elements in either a or b but not both (symmetric difference).

vec_tail

Return all but the first element (i.e. tail of the vector).

vec_take

Take up to n elements from the front of a slice.

vec_take_while

Take elements while a predicate is true.

vec_transpose

Transpose a Vec<Vec<T>> (rows ↔ columns).

vec_try_map

Map a fallible function over a vector, returning early on error.

vec_unzip

Unzip a vector of pairs into two vectors.

vec_variance_f64

Compute the variance (population) of a f64 slice.

vec_zip

Zip two vectors into a vector of pairs (up to the shorter length).

windows_collect

Sliding window iterator: produce all sub-slices of length window.

zip_exact

Zip two slices, failing if they have different lengths.