Module functions_2 

Auto-generated module

🤖 Generated with SplitRS

Functions

arr_ext_array2d_ty

Array2D : Type → Nat → Nat → Type

arr_ext_chunks_cover_ty

Array.chunks_cover : ∀ {α n k}, Array α n → Prop

arr_ext_chunks_of_ty

Array.chunksOf : {α : Type} → {n : Nat} → Nat → Array α n → List (List α)

arr_ext_convolution_ty

Array.convolution : {n : Nat} → Array Nat n → Array Nat n → Array Nat n

arr_ext_diff_array_ty

Array.diff_array : {α : Type} → {n : Nat} → Array α n → Array α n

arr_ext_fft_conv_correct_ty

Array.fft_conv_correct : ∀ {n}, Array Nat n → Array Nat n → Prop

arr_ext_filter_map_fuse_ty

Array.filter_map_fuse : ∀ {α β n}, (α → Option β) → Array α n → Prop

arr_ext_fold_map_fuse_ty

Array.fold_map_fuse : ∀ {α β γ n}, (β → γ → γ) → γ → (α → β) → Array α n → Prop

arr_ext_map_fuse_ty

Array.map_fuse : ∀ {α β γ n}, (β → γ) → (α → β) → Array α n → Prop

arr_ext_par_map_correct_ty

Array.par_map_correct : ∀ {α β n}, (α → β) → Array α n → Prop

arr_ext_par_map_ty

Array.par_map : {α β : Type} → {n : Nat} → (α → β) → Array α n → Array β n

arr_ext_par_reduce_ty

Array.par_reduce : {α : Type} → {n : Nat} → (α → α → α) → α → Array α n → α

arr_ext_persistent_array_ty

PersistentArray : Type → Nat → Type

arr_ext_persistent_get_ty

PersistentArray.get : {α : Type} → {n : Nat} → PersistentArray α n → Fin n → α

arr_ext_persistent_set_ty

PersistentArray.set : {α : Type} → {n : Nat} → PersistentArray α n → Fin n → α → PersistentArray α n

arr_ext_prefix_sum_correct_ty

Array.prefix_sum_correct : ∀ {n}, Array Nat n → Prop

arr_ext_rmq_correct_ty

Array.rmq_correct : ∀ {α n}, [Ord α] → Array α n → Prop

arr_ext_rotate_inverse_ty

Array.rotate_inverse : ∀ {α n k}, Array α n → Prop

arr_ext_rotate_left_ty

Array.rotate_left : {α : Type} → {n : Nat} → Nat → Array α n → Array α n

arr_ext_rotate_right_ty

Array.rotate_right : {α : Type} → {n : Nat} → Nat → Array α n → Array α n

arr_ext_scan_left_ty

Array.scan_left : {α β : Type} → {n : Nat} → (β → α → β) → β → Array α n → Array β (n+1)

arr_ext_sparse_table_ty

Array.sparse_table : {α : Type} → {n : Nat} → [Ord α] → Array α n → Type

arr_ext_suffix_array_correct_ty

Array.suffix_array_correct : ∀ {n}, Array Nat n → Prop

arr_ext_suffix_array_ty

Array.suffix_array : {n : Nat} → Array Nat n → Array Nat n

arr_ext_transpose_ty

Array2D.transpose : {α : Type} → {r c : Nat} → Array2D α r c → Array2D α c r

merge_sort

Merge sort implementation on a mutable slice.

register_array_extended

Register all extended array axioms into the kernel environment.