Array literal syntax #
Equations
Instances For
Preliminary theorems #
Equations
- Array.instMembership = { mem := Array.Mem }
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Externs #
Returns the size of the array as a platform-native unsigned integer.
This is a low-level version of Array.size
that directly queries the runtime system's
representation of arrays. While this is not provable, Array.usize
always returns the exact size of
the array since the implementation only supports arrays of size less than USize.size
.
Instances For
Low-level modification operator which is as fast as a C array write. The modification is performed in-place when the reference to the array is unique.
This avoids overhead due to unboxing a Nat
used as an index.
Instances For
Removes the last element of an array. If the array is empty, then it is returned unmodified. The modification is performed in-place when the reference to the array is unique.
Examples:
Instances For
Creates an array that contains n
repetitions of v
.
The corresponding List
function is List.replicate
.
Examples:
Array.replicate 2 true = #[true, true]
Array.replicate 3 () = #[(), (), ()]
Array.replicate 0 "anything" = #[]
Equations
- Array.replicate n v = { toList := List.replicate n v }
Instances For
Creates an array that contains n
repetitions of v
.
The corresponding List
function is List.replicate
.
Examples:
Array.mkArray 2 true = #[true, true]
Array.mkArray 3 () = #[(), (), ()]
Array.mkArray 0 "anything" = #[]
Equations
- mkArray n v = { toList := List.replicate n v }
Instances For
Swaps two elements of an array. The modification is performed in-place when the reference to the array is unique.
Examples:
#["red", "green", "blue", "brown"].swap 0 3 = #["brown", "green", "blue", "red"]
#["red", "green", "blue", "brown"].swap 0 2 = #["blue", "green", "red", "brown"]
#["red", "green", "blue", "brown"].swap 1 2 = #["red", "blue", "green", "brown"]
#["red", "green", "blue", "brown"].swap 3 0 = #["brown", "green", "blue", "red"]
Instances For
Swaps two elements of an array, returning the array unchanged if either index is out of bounds. The modification is performed in-place when the reference to the array is unique.
Examples:
#["red", "green", "blue", "brown"].swapIfInBounds 0 3 = #["brown", "green", "blue", "red"]
#["red", "green", "blue", "brown"].swapIfInBounds 0 2 = #["blue", "green", "red", "brown"]
#["red", "green", "blue", "brown"].swapIfInBounds 1 2 = #["red", "blue", "green", "brown"]
#["red", "green", "blue", "brown"].swapIfInBounds 0 4 = #["red", "green", "blue", "brown"]
#["red", "green", "blue", "brown"].swapIfInBounds 9 2 = #["red", "green", "blue", "brown"]
Equations
Instances For
Equations
Instances For
Definitions #
Equations
- Array.instEmptyCollection = { emptyCollection := #[] }
Equations
- Array.instInhabited = { default := #[] }
Returns true
if as
and bs
have the same length and they are pairwise related by eqv
.
Short-circuits at the first non-related pair of elements.
Examples:
#[1, 2, 3].isEqv #[2, 3, 4] (· < ·) = true
#[1, 2, 3].isEqv #[2, 2, 4] (· < ·) = false
#[1, 2, 3].isEqv #[2, 3] (· < ·) = false
Instances For
Creates an array by applying f
to each potential index in order, starting at 0
.
Examples:
Array.ofFn (n := 3) toString = #["0", "1", "2"]
Array.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = #["red", "green", "blue"]
Equations
- Array.ofFn f = Array.ofFn.go f 0 (Array.emptyWithCapacity n)
Instances For
Constructs an array that contains all the numbers from 0
to n
, exclusive.
Examples:
Array.range 5 := #[0, 1, 2, 3, 4]
Array.range 0 := #[]
Array.range 1 := #[0]
Equations
- Array.range n = Array.ofFn fun (i : Fin n) => ↑i
Instances For
Constructs an array of numbers of size size
, starting at start
and increasing by
step
at each element.
In other words, Array.range' start size step
is #[start, start+step, ..., start+(len-1)*step]
.
Examples:
Array.range' 0 3 (step := 1) = #[0, 1, 2]
Array.range' 0 3 (step := 2) = #[0, 2, 4]
Array.range' 0 4 (step := 2) = #[0, 2, 4, 6]
Array.range' 3 4 (step := 2) = #[3, 5, 7, 9]
Equations
- Array.range' start size step = Array.ofFn fun (i : Fin size) => start + step * ↑i
Instances For
Constructs a single-element array that contains v
.
Examples:
Array.singleton 5 = #[5]
Array.singleton "one" = #["one"]
Equations
- Array.singleton v = #[v]
Instances For
Returns the last element of an array, or panics if the array is empty.
Safer alternatives include Array.back
, which requires a proof the array is non-empty, and
Array.back?
, which returns an Option
.
Instances For
Returns the last element of an array, given a proof that the array is not empty.
See Array.back!
for the version that panics if the array is empty, or Array.back?
for the
version that returns an option.
Instances For
Returns the last element of an array, or none
if the array is empty.
See Array.back!
for the version that panics if the array is empty, or Array.back
for the version
that requires a proof the array is non-empty.
Instances For
Swaps a new element with the element at the given index.
Returns the value formerly found at i
, paired with an array in which the value at i
has been
replaced with v
.
Examples:
#["spinach", "broccoli", "carrot"].swapAt 1 "pepper" = ("broccoli", #["spinach", "pepper", "carrot"])
#["spinach", "broccoli", "carrot"].swapAt 2 "pepper" = ("carrot", #["spinach", "broccoli", "pepper"])
Instances For
Swaps a new element with the element at the given index. Panics if the index is out of bounds.
Returns the value formerly found at i
, paired with an array in which the value at i
has been
replaced with v
.
Examples:
#["spinach", "broccoli", "carrot"].swapAt! 1 "pepper" = (#["spinach", "pepper", "carrot"], "broccoli")
#["spinach", "broccoli", "carrot"].swapAt! 2 "pepper" = (#["spinach", "broccoli", "pepper"], "carrot")
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns the first n
elements of an array. The resulting array is produced by repeatedly calling
Array.pop
. If n
is greater than the size of the array, it is returned unmodified.
If the reference to the array is unique, then this function uses in-place modification.
Examples:
#[0, 1, 2, 3, 4].shrink 2 = #[0, 1]
#[0, 1, 2, 3, 4].shrink 0 = #[]
#[0, 1, 2, 3, 4].shrink 10 = #[0, 1, 2, 3, 4]
Equations
- xs.shrink n = Array.shrink.loop (xs.size - n) xs
Instances For
Equations
- Array.shrink.loop 0 x✝ = x✝
- Array.shrink.loop n.succ x✝ = Array.shrink.loop n x✝.pop
Instances For
Returns a new array that contains the first i
elements of xs
. If xs
has fewer than i
elements, the new array contains all the elements of xs
.
The returned array is always a new array, even if it contains the same elements as the input array.
Examples:
#["red", "green", "blue"].take 1 = #["red"]
#["red", "green", "blue"].take 2 = #["red", "green"]
#["red", "green", "blue"].take 5 = #["red", "green", "blue"]
Instances For
Removes the first i
elements of xs
. If xs
has fewer than i
elements, the new array is empty.
The returned array is always a new array, even if it contains the same elements as the input array.
Examples:
#["red", "green", "blue"].drop 1 = #["green", "blue"]
#["red", "green", "blue"].drop 2 = #["blue"]
#["red", "green", "blue"].drop 5 = #[]
Instances For
Replaces the element at the given index, if it exists, with the result of applying the monadic
function f
to it. If the index is invalid, the array is returned unmodified and f
is not called.
Examples:
#eval #[1, 2, 3, 4].modifyM 2 fun x => do
IO.println s!"It was {x}"
return x * 10
It was 3
#[1, 2, 30, 4]
#eval #[1, 2, 3, 4].modifyM 6 fun x => do
IO.println s!"It was {x}"
return x * 10
#[1, 2, 3, 4]
Equations
Instances For
Replaces the element at the given index, if it exists, with the result of applying f
to it. If the
index is invalid, the array is returned unmodified.
Examples:
#[1, 2, 3].modify 0 (· * 10) = #[10, 2, 3]
#[1, 2, 3].modify 2 (· * 10) = #[1, 2, 30]
#[1, 2, 3].modify 3 (· * 10) = #[1, 2, 3]
Instances For
Replaces the element at the given index, if it exists, with the result of applying f
to it. If the
index is invalid, the array is returned unmodified.
Examples:
#[1, 2, 3].modifyOp 0 (· * 10) = #[10, 2, 3]
#[1, 2, 3].modifyOp 2 (· * 10) = #[1, 2, 30]
#[1, 2, 3].modifyOp 3 (· * 10) = #[1, 2, 3]
Instances For
We claim this unsafe implementation is correct because an array cannot have more than usizeSz
elements in our runtime.
This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies as.size < usizeSz
to true.
Equations
- as.forIn'Unsafe b f = Array.forIn'Unsafe.loop as f as.usize 0 b
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Array.forIn'.loop as f 0 x_2 b = pure b
Instances For
Equations
- Array.instForIn'InferInstanceMembership = { forIn' := fun {β : Type ?u.14} [Monad m] => Array.forIn' }
See comment at forIn'Unsafe
Equations
- Array.foldlMUnsafe f init as start stop = if start < stop then if stop ≤ as.size then Array.foldlMUnsafe.fold f as (USize.ofNat start) (USize.ofNat stop) init else pure init else pure init
Instances For
Folds a monadic function over a list from the left, accumulating a value starting with init
. The
accumulated value is combined with the each element of the list in order, using f
.
The optional parameters start
and stop
control the region of the array to be folded. Folding
proceeds from start
(inclusive) to stop
(exclusive), so no folding occurs unless start < stop
.
By default, the entire array is folded.
Examples:
example [Monad m] (f : α → β → m α) :
Array.foldlM (m := m) f x₀ #[a, b, c] = (do
let x₁ ← f x₀ a
let x₂ ← f x₁ b
let x₃ ← f x₂ c
pure x₃)
:= by rfl
example [Monad m] (f : α → β → m α) :
Array.foldlM (m := m) f x₀ #[a, b, c] (start := 1) = (do
let x₁ ← f x₀ b
let x₂ ← f x₁ c
pure x₂)
:= by rfl
Equations
- One or more equations did not get rendered due to their size.
Instances For
Folds a monadic function over an array from the right, accumulating a value starting with init
.
The accumulated value is combined with the each element of the list in reverse order, using f
.
The optional parameters start
and stop
control the region of the array to be folded. Folding
proceeds from start
(exclusive) to stop
(inclusive), so no folding occurs unless start > stop
.
By default, the entire array is folded.
Examples:
example [Monad m] (f : α → β → m β) :
Array.foldrM (m := m) f x₀ #[a, b, c] = (do
let x₁ ← f c x₀
let x₂ ← f b x₁
let x₃ ← f a x₂
pure x₃)
:= by rfl
example [Monad m] (f : α → β → m β) :
Array.foldrM (m := m) f x₀ #[a, b, c] (start := 2) = (do
let x₁ ← f b x₀
let x₂ ← f a x₁
pure x₂)
:= by rfl
Equations
- One or more equations did not get rendered due to their size.
Instances For
See comment at forIn'Unsafe
Equations
- Array.mapMUnsafe f as = unsafeCast (Array.mapMUnsafe.map f as.usize 0 (unsafeCast as))
Instances For
Applies the monadic action f
to every element in the array, left-to-right, and returns the array
of results.
Equations
- Array.mapM f as = Array.mapM.map f as 0 (Array.emptyWithCapacity as.size)
Instances For
Equations
- Array.mapM.map f as i bs = if hlt : i < as.size then do let __do_lift ← f as[i] Array.mapM.map f as (i + 1) (bs.push __do_lift) else pure bs
Instances For
Applies the monadic action f
to every element in the array, along with the element's index and a
proof that the index is in bounds, from left to right. Returns the array of results.
Equations
- as.mapFinIdxM f = Array.mapFinIdxM.map as f as.size 0 ⋯ (Array.emptyWithCapacity as.size)
Instances For
Equations
- Array.mapFinIdxM.map as f 0 j x bs = pure bs
- Array.mapFinIdxM.map as f i_2.succ j inv_2 bs = do let __do_lift ← f j as[j] ⋯ Array.mapFinIdxM.map as f i_2 (j + 1) ⋯ (bs.push __do_lift)
Instances For
Applies the monadic action f
to every element in the array, along with the element's index, from
left to right. Returns the array of results.
Equations
- Array.mapIdxM f as = as.mapFinIdxM fun (i : Nat) (a : α) (x : i < as.size) => f i a
Instances For
Maps f
over the array and collects the results with <|>
. The result for the end of the array is
failure
.
Examples:
#[[], [1, 2], [], [2]].firstM List.head? = some 1
#[[], [], []].firstM List.head? = none
#[].firstM List.head? = none
Equations
- Array.firstM f as = Array.firstM.go f as 0
Instances For
Equations
- Array.firstM.go f as i = if hlt : i < as.size then f as[i] <|> Array.firstM.go f as (i + 1) else failure
Instances For
Returns the first non-none
result of applying the monadic function f
to each element of the
array, in order. Returns none
if f
returns none
for all elements.
Example:
#eval #[7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
if i < 5 then
return some (i * 10)
if i ≤ 6 then
IO.println s!"Almost! {i}"
return none
Almost! 6
Almost! 5
some 10
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns the first element of the array for which the monadic predicate p
returns true
, or none
if no such element is found. Elements of the array are checked in order.
The monad m
is restricted to Type → Type
to avoid needing to use ULift Bool
in p
's type.
Example:
#eval #[7, 6, 5, 8, 1, 2, 6].findM? fun i => do
if i < 5 then
return true
if i ≤ 6 then
IO.println s!"Almost! {i}"
return false
Almost! 6
Almost! 5
some 1
Equations
- One or more equations did not get rendered due to their size.
Instances For
Finds the index of the first element of an array for which the monadic predicate p
returns true
.
Elements are examined in order from left to right, and the search is terminated when an element that
satisfies p
is found. If no such element exists in the array, then none
is returned.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if the monadic predicate p
returns true
for any element of as
.
Short-circuits upon encountering the first true
. The elements in as
are examined in order from
left to right.
The optional parameters start
and stop
control the region of the array to be checked. Only the
elements with indices from start
(inclusive) to stop
(exclusive) are checked. By default, the
entire array is checked.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns true
if the monadic predicate p
returns true
for every element of as
.
Short-circuits upon encountering the first false
. The elements in as
are examined in order from
left to right.
The optional parameters start
and stop
control the region of the array to be checked. Only the
elements with indices from start
(inclusive) to stop
(exclusive) are checked. By default, the
entire array is checked.
Equations
- Array.allM p as start stop = do let __do_lift ← Array.anyM (fun (v : α) => do let __do_lift ← p v pure !__do_lift) as start stop pure !__do_lift
Instances For
Returns the first non-none
result of applying the monadic function f
to each element of the
array in reverse order, from right to left. Once a non-none
result is found, no further elements
are checked. Returns none
if f
returns none
for all elements of the array.
Examples:
#eval #[1, 2, 0, -4, 1].findSomeRevM? (m := Except String) fun x => do
if x = 0 then throw "Zero!"
else if x < 0 then return (some x)
else return none
Except.ok (some (-4))
#eval #[1, 2, 0, 4, 1].findSomeRevM? (m := Except String) fun x => do
if x = 0 then throw "Zero!"
else if x < 0 then return (some x)
else return none
Except.error "Zero!"
Equations
- Array.findSomeRevM? f as = Array.findSomeRevM?.find f as as.size ⋯
Instances For
Equations
- Array.findSomeRevM?.find f as 0 x_2 = pure none
- Array.findSomeRevM?.find f as i.succ h = do let r ← f as[i] match r with | some val => pure r | none => let_fun this := ⋯; Array.findSomeRevM?.find f as i this
Instances For
Returns the last element of the array for which the monadic predicate p
returns true
, or none
if no such element is found. Elements of the array are checked in reverse, from right to left..
The monad m
is restricted to Type → Type
to avoid needing to use ULift Bool
in p
's type.
Example:
#eval #[7, 5, 8, 1, 2, 6, 5, 8].findRevM? fun i => do
if i < 5 then
return true
if i ≤ 6 then
IO.println s!"Almost! {i}"
return false
Almost! 5
Almost! 6
some 2
Equations
Instances For
Applies the monadic action f
to each element of an array, in order.
The optional parameters start
and stop
control the region of the array to which f
should be
applied. Iteration proceeds from start
(inclusive) to stop
(exclusive), so f
is not invoked
unless start < stop
. By default, the entire array is used.
Equations
- Array.forM f as start stop = Array.foldlM (fun (x : PUnit) => f) PUnit.unit as start stop
Instances For
Equations
- Array.instForM = { forM := fun [Monad m] (xs : Array α) (f : α → m PUnit) => Array.forM f xs }
Applies the monadic action f
to each element of an array from right to left, in reverse order.
The optional parameters start
and stop
control the region of the array to which f
should be
applied. Iteration proceeds from start
(exclusive) to stop
(inclusive), so no f
is not invoked
unless start > stop
. By default, the entire array is used.
Equations
- Array.forRevM f as start stop = Array.foldrM (fun (a : α) (x : PUnit) => f a) PUnit.unit as start stop
Instances For
Folds a function over an array from the left, accumulating a value starting with init
. The
accumulated value is combined with the each element of the array in order, using f
.
The optional parameters start
and stop
control the region of the array to be folded. Folding
proceeds from start
(inclusive) to stop
(exclusive), so no folding occurs unless start < stop
.
By default, the entire array is used.
Examples:
#[a, b, c].foldl f z = f (f (f z a) b) c
#[1, 2, 3].foldl (· ++ toString ·) "" = "123"
#[1, 2, 3].foldl (s!"({·} {·})") "" = "((( 1) 2) 3)"
Equations
- Array.foldl f init as start stop = (Array.foldlM f init as start stop).run
Instances For
Folds a function over an array from the right, accumulating a value starting with init
. The
accumulated value is combined with the each element of the array in reverse order, using f
.
The optional parameters start
and stop
control the region of the array to be folded. Folding
proceeds from start
(exclusive) to stop
(inclusive), so no folding occurs unless start > stop
.
By default, the entire array is used.
Examples:
#[a, b, c].foldr f init = f a (f b (f c init))
#[1, 2, 3].foldr (toString · ++ ·) "" = "123"
#[1, 2, 3].foldr (s!"({·} {·})") "!" = "(1 (2 (3 !)))"
Equations
- Array.foldr f init as start stop = (Array.foldrM f init as start stop).run
Instances For
Counts the number of elements in the array as
that satisfy the Boolean predicate p
.
Examples:
#[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2
#[1, 2, 3, 4, 5].countP (· < 5) = 4
#[1, 2, 3, 4, 5].countP (· > 5) = 0
Equations
- Array.countP p as = Array.foldr (fun (a : α) (acc : Nat) => bif p a then acc + 1 else acc) 0 as
Instances For
Counts the number of times an element occurs in an array.
Examples:
Equations
- Array.count a as = Array.countP (fun (x : α) => x == a) as
Instances For
Applies a function to each element of the array, returning the resulting array of values.
Examples:
#[a, b, c].map f = #[f a, f b, f c]
#[].map Nat.succ = #[]
#["one", "two", "three"].map (·.length) = #[3, 3, 5]
#["one", "two", "three"].map (·.reverse) = #["eno", "owt", "eerht"]
Equations
- Array.map f as = (Array.mapM f as).run
Instances For
Equations
- Array.instFunctor = { map := fun {α β : Type ?u.9} => Array.map }
Applies a function to each element of the array along with the index at which that element is found, returning the array of results. In addition to the index, the function is also provided with a proof that the index is valid.
Array.mapIdx
is a variant that does not provide the function with evidence that the index is
valid.
Equations
- as.mapFinIdx f = (as.mapFinIdxM f).run
Instances For
Applies a function to each element of the array along with the index at which that element is found, returning the array of results.
Array.mapFinIdx
is a variant that additionally provides the function with a proof that the index
is valid.
Equations
- Array.mapIdx f as = (Array.mapIdxM f as).run
Instances For
Pairs each element of an array with its index, optionally starting from an index other than 0
.
Examples:
Instances For
Equations
Instances For
Returns the first element of the array for which the predicate p
returns true
, or none
if no
such element is found.
Examples:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns the first non-none
result of applying the function f
to each element of the
array, in order. Returns none
if f
returns none
for all elements.
Example:
#eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i =>
if i < 5 then
some (i * 10)
else
none
some 10
Equations
- Array.findSome? f as = (Array.findSomeM? f as).run
Instances For
Returns the first non-none
result of applying the function f
to each element of the
array, in order. Panics if f
returns none
for all elements.
Example:
#eval #[7, 6, 5, 8, 1, 2, 6].findSome? fun i =>
if i < 5 then
some (i * 10)
else
none
some 10
Equations
- Array.findSome! f xs = match Array.findSome? f xs with | some b => b | none => panicWithPosWithDecl "Init.Data.Array.Basic" "Array.findSome!" 1219 14 "failed to find element"
Instances For
Returns the first non-none
result of applying f
to each element of the array in reverse order,
from right to left. Returns none
if f
returns none
for all elements of the array.
Examples:
#[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 5 then some (10 * x) else none) = some 10
#[7, 6, 5, 8, 1, 2, 6].findSome? (fun x => if x < 1 then some (10 * x) else none) = none
Equations
- Array.findSomeRev? f as = (Array.findSomeRevM? f as).run
Instances For
Returns the last element of the array for which the predicate p
returns true
, or none
if no
such element is found.
Examples:
Equations
- Array.findRev? p as = (Array.findRevM? p as).run
Instances For
Returns the index of the first element for which p
returns true
, or none
if there is no such
element.
Examples:
Equations
- Array.findIdx? p as = Array.findIdx?.loop p as 0
Instances For
Returns the index of the first element for which p
returns true
, or none
if there is no such
element. The index is returned as a Fin
, which guarantees that it is in bounds.
Examples:
#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)
#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none
Equations
- Array.findFinIdx? p as = Array.findFinIdx?.loop p as 0
Instances For
Returns the index of the first element for which p
returns true
, or the size of the array if
there is no such element.
Examples:
Equations
- Array.findIdx p as = (Array.findIdx? p as).getD as.size
Instances For
Equations
Instances For
Returns the index of the first element equal to a
, or the size of the array if no element is equal
to a
. The index is returned as a Fin
, which guarantees that it is in bounds.
Examples:
#["carrot", "potato", "broccoli"].finIdxOf? "carrot" = some 0
#["carrot", "potato", "broccoli"].finIdxOf? "broccoli" = some 2
#["carrot", "potato", "broccoli"].finIdxOf? "tomato" = none
#["carrot", "potato", "broccoli"].finIdxOf? "anything else" = none
Instances For
Equations
Instances For
Returns the index of the first element equal to a
, or the size of the array if no element is equal
to a
.
Examples:
#["carrot", "potato", "broccoli"].idxOf "carrot" = 0
#["carrot", "potato", "broccoli"].idxOf "broccoli" = 2
#["carrot", "potato", "broccoli"].idxOf "tomato" = 3
#["carrot", "potato", "broccoli"].idxOf "anything else" = 3
Equations
- Array.idxOf a = Array.findIdx fun (x : α) => x == a
Instances For
Returns the index of the first element equal to a
, or none
if no element is equal to a
.
Examples:
#["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0
#["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2
#["carrot", "potato", "broccoli"].idxOf? "tomato" = none
#["carrot", "potato", "broccoli"].idxOf? "anything else" = none
Instances For
Returns true
if p
returns true
for any element of as
.
Short-circuits upon encountering the first true
.
The optional parameters start
and stop
control the region of the array to be checked. Only the
elements with indices from start
(inclusive) to stop
(exclusive) are checked. By default, the
entire array is checked.
Examples:
#[2, 4, 6].any (· % 2 = 0) = true
#[2, 4, 6].any (· % 2 = 1) = false
#[2, 4, 5, 6].any (· % 2 = 0) = true
#[2, 4, 5, 6].any (· % 2 = 1) = true
Equations
- as.any p start stop = (Array.anyM p as start stop).run
Instances For
Returns true
if p
returns true
for every element of as
.
Short-circuits upon encountering the first false
.
The optional parameters start
and stop
control the region of the array to be checked. Only the
elements with indices from start
(inclusive) to stop
(exclusive) are checked. By default, the
entire array is checked.
Examples:
#[a, b, c].all p = (p a && (p b && p c))
#[2, 4, 6].all (· % 2 = 0) = true
#[2, 4, 5, 6].all (· % 2 = 0) = false
Equations
- as.all p start stop = (Array.allM p as start stop).run
Instances For
Checks whether a
is an element of as
, using ==
to compare elements.
Array.elem
is a synonym that takes the element before the array.
Examples:
#[1, 4, 2, 3, 3, 7].contains 3 = true
Array.contains #[1, 4, 2, 3, 3, 7] 5 = false
Instances For
Checks whether a
is an element of as
, using ==
to compare elements.
Array.contains
is a synonym that takes the array before the element.
For verification purposes, Array.elem
is simplified to Array.contains
.
Example:
Array.elem 3 #[1, 4, 2, 3, 3, 7] = true
Array.elem 5 #[1, 4, 2, 3, 3, 7] = false
Equations
- Array.elem a as = as.contains a
Instances For
Convert a Array α
into an List α
. This is O(n) in the size of the array.
Equations
- as.toListImpl = Array.foldr List.cons [] as
Instances For
Prepends an array to a list. The elements of the array are at the beginning of the resulting list.
Equivalent to as.toList ++ l
.
Examples:
#[1, 2].toListAppend [3, 4] = [1, 2, 3, 4]
#[1, 2].toListAppend [] = [1, 2]
#[].toListAppend [3, 4, 5] = [3, 4, 5]
Equations
- as.toListAppend l = Array.foldr List.cons l as
Instances For
Appends two arrays. Normally used via the ++
operator.
Appending arrays takes time proportional to the length of the second array.
Examples:
#[1, 2, 3] ++ #[4, 5] = #[1, 2, 3, 4, 5]
.#[] ++ #[4, 5] = #[4, 5]
.#[1, 2, 3] ++ #[] = #[1, 2, 3]
.
Equations
- as.append bs = Array.foldl (fun (xs : Array α) (v : α) => xs.push v) as bs
Instances For
Equations
- Array.instAppend = { append := Array.append }
Appends an array and a list.
Takes time proportional to the length of the list..
Examples:
#[1, 2, 3].appendList [4, 5] = #[1, 2, 3, 4, 5]
.#[].appendList [4, 5] = #[4, 5]
.#[1, 2, 3].appendList [] = #[1, 2, 3]
.
Equations
- as.appendList bs = List.foldl (fun (xs : Array α) (v : α) => xs.push v) as bs
Instances For
Equations
- Array.instHAppendList = { hAppend := Array.appendList }
Applies a monadic function that returns an array to each element of an array, from left to right. The resulting arrays are appended.
Equations
- Array.flatMapM f as = Array.foldlM (fun (bs : Array β) (a : α) => do let __do_lift ← f a pure (bs ++ __do_lift)) #[] as
Instances For
Applies a function that returns an array to each element of an array. The resulting arrays are appended.
Examples:
#[2, 3, 2].flatMap Array.range = #[0, 1, 0, 1, 2, 0, 1]
#[['a', 'b'], ['c', 'd', 'e']].flatMap List.toArray = #['a', 'b', 'c', 'd', 'e']
Equations
- Array.flatMap f as = Array.foldl (fun (bs : Array β) (a : α) => bs ++ f a) #[] as
Instances For
Equations
Instances For
Appends the contents of array of arrays into a single array. The resulting array contains the same elements as the nested arrays in the same order.
Examples:
#[#[5], #[4], #[3, 2]].flatten = #[5, 4, 3, 2]
#[#[0, 1], #[], #[2], #[1, 0, 1]].flatten = #[0, 1, 2, 1, 0, 1]
(#[] : Array Nat).flatten = #[]
Instances For
Reverses an array by repeatedly swapping elements.
The original array is modified in place if there are no other references to it.
Examples:
Instances For
Equations
- Array.reverse.loop as i j = if h : i < ↑j then let_fun this := ⋯; let as_1 := as.swap i ↑j ⋯ ⋯; let_fun this := ⋯; Array.reverse.loop as_1 (i + 1) ⟨↑j - 1, this⟩ else as
Instances For
Returns the array of elements in as
for which p
returns true
.
Only elements from start
(inclusive) to stop
(exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is considered.
Examples:
#[1, 2, 5, 2, 7, 7].filter (· > 2) = #[5, 7, 7]
#[1, 2, 5, 2, 7, 7].filter (fun _ => false) = #[]
#[1, 2, 5, 2, 7, 7].filter (fun _ => true) = #[1, 2, 5, 2, 7, 7]
#[1, 2, 5, 2, 7, 7].filter (· > 2) (start := 3) = #[7, 7]
#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (start := 3) = #[2, 7, 7]
#[1, 2, 5, 2, 7, 7].filter (fun _ => true) (stop := 3) = #[1, 2, 5]
Equations
Instances For
Applies the monadic predicate p
to every element in the array, in order from left to right, and
returns the array of elements for which p
returns true
.
Only elements from start
(inclusive) to stop
(exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is checked.
Example:
#eval #[1, 2, 5, 2, 7, 7].filterM fun x => do
IO.println s!"Checking {x}"
return x < 3
Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7
#[1, 2, 2]
Equations
Instances For
Applies the monadic predicate p
on every element in the array in reverse order, from right to
left, and returns those elements for which p
returns true
. The elements of the returned list are
in the same order as in the input list.
Only elements from start
(exclusive) to stop
(inclusive) are considered. Elements outside that
range are discarded. Because the array is examined in reverse order, elements are only examined when
start > stop
. By default, the entire array is considered.
Example:
#eval #[1, 2, 5, 2, 7, 7].filterRevM fun x => do
IO.println s!"Checking {x}"
return x < 3
Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1
#[1, 2, 2]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Applies a monadic function that returns an Option
to each element of an array, collecting the
non-none
values.
Only elements from start
(inclusive) to stop
(exclusive) are considered. Elements outside that
range are discarded. By default, the entire array is considered.
Example:
#eval #[1, 2, 5, 2, 7, 7].filterMapM fun x => do
IO.println s!"Examining {x}"
if x > 2 then return some (2 * x)
else return none
Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7
#[10, 14, 14]
Equations
- One or more equations did not get rendered due to their size.
Instances For
Applies a function that returns an Option
to each element of an array, collecting the non-none
values.
Example:
#eval #[1, 2, 5, 2, 7, 7].filterMap fun x =>
if x > 2 then some (2 * x) else none
#[10, 14, 14]
Equations
- Array.filterMap f as start stop = (Array.filterMapM f as start stop).run
Instances For
Returns the largest element of the array, as determined by the comparison lt
, or none
if
the array is empty.
Examples:
(#[] : Array Nat).getMax? (· < ·) = none
#["red", "green", "blue"].getMax? (·.length < ·.length) = some "green"
#["red", "green", "blue"].getMax? (· < ·) = some "red"
Equations
Instances For
Returns a pair of arrays that together contain all the elements of as
. The first array contains
those elements for which p
returns true
, and the second contains those for which p
returns
false
.
as.partition p
is equivalent to (as.filter p, as.filter (not ∘ p))
, but it is
more efficient since it only has to do one pass over the array.
Examples:
#[1, 2, 5, 2, 7, 7].partition (· > 2) = (#[5, 7, 7], #[1, 2, 2])
#[1, 2, 5, 2, 7, 7].partition (fun _ => false) = (#[], #[1, 2, 5, 2, 7, 7])
#[1, 2, 5, 2, 7, 7].partition (fun _ => true) = (#[1, 2, 5, 2, 7, 7], #[])
Equations
- One or more equations did not get rendered due to their size.
Instances For
Removes all the elements that satisfy a predicate from the end of an array.
The longest contiguous sequence of elements that all satisfy the predicate is removed.
Examples:
#[0, 1, 2, 3, 4].popWhile (· > 2) = #[0, 1, 2]
#[3, 2, 3, 4].popWhile (· > 2) = #[3, 2]
(#[] : Array Nat).popWhile (· > 2) = #[]
Equations
Instances For
Returns a new array that contains the longest prefix of elements that satisfy the predicate p
from
an array.
Examples:
#[0, 1, 2, 3, 2, 1].takeWhile (· < 2) = #[0, 1]
#[0, 1, 2, 3, 2, 1].takeWhile (· < 20) = #[0, 1, 2, 3, 2, 1]
#[0, 1, 2, 3, 2, 1].takeWhile (· < 0) = #[]
Equations
- Array.takeWhile p as = Array.takeWhile.go p as 0 #[]
Instances For
Removes the element at a given index from an array without a run-time bounds check.
This function takes worst-case O(n)
time because it back-shifts all elements at positions
greater than i
.
Examples:
#["apple", "pear", "orange"].eraseIdx 0 = #["pear", "orange"]
#["apple", "pear", "orange"].eraseIdx 1 = #["apple", "orange"]
#["apple", "pear", "orange"].eraseIdx 2 = #["apple", "pear"]
Equations
Instances For
Removes the element at a given index from an array. Does nothing if the index is out of bounds.
This function takes worst-case O(n)
time because it back-shifts all elements at positions greater
than i
.
Examples:
#["apple", "pear", "orange"].eraseIdxIfInBounds 0 = #["pear", "orange"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 1 = #["apple", "orange"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 2 = #["apple", "pear"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 3 = #["apple", "pear", "orange"]
#["apple", "pear", "orange"].eraseIdxIfInBounds 5 = #["apple", "pear", "orange"]
Equations
- xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i h else xs
Instances For
Removes the element at a given index from an array. Panics if the index is out of bounds.
This function takes worst-case O(n)
time because it back-shifts all elements at positions
greater than i
.
Equations
Instances For
Removes the first occurrence of a specified element from an array, or does nothing if it is not present.
This function takes worst-case O(n)
time because it back-shifts all later elements.
Examples:
#[1, 2, 3].erase 2 = #[1, 3]
#[1, 2, 3].erase 5 = #[1, 2, 3]
#[1, 2, 3, 2, 1].erase 2 = #[1, 3, 2, 1]
(#[] : List Nat).erase 2 = #[]
Instances For
Removes the first element that satisfies the predicate p
. If no element satisfies p
, the array
is returned unmodified.
This function takes worst-case O(n)
time because it back-shifts all later elements.
Examples:
#["red", "green", "", "blue"].eraseP (·.isEmpty) = #["red", "green", "blue"]
#["red", "green", "", "blue", ""].eraseP (·.isEmpty) = #["red", "green", "blue", ""]
#["red", "green", "blue"].eraseP (·.length % 2 == 0) = #["red", "green"]
#["red", "green", "blue"].eraseP (fun _ => true) = #["green", "blue"]
(#[] : Array String).eraseP (fun _ => true) = #[]
Instances For
Inserts an element into an array at the specified index. If the index is greater than the size of the array, then the array is returned unmodified.
In other words, the new element is inserted into the array as
after the first i
elements of
as
.
This function takes worst case O(n)
time because it has to swap the inserted element into place.
Examples:
#["tues", "thur", "sat"].insertIdx 1 "wed" = #["tues", "wed", "thur", "sat"]
#["tues", "thur", "sat"].insertIdx 2 "wed" = #["tues", "thur", "wed", "sat"]
#["tues", "thur", "sat"].insertIdx 3 "wed" = #["tues", "thur", "sat", "wed"]
Equations
- as.insertIdx i a x✝ = Array.insertIdx.loop i (as.push a) ⟨as.size, ⋯⟩
Instances For
Equations
Instances For
Inserts an element into an array at the specified index. Panics if the index is greater than the size of the array.
In other words, the new element is inserted into the array as
after the first i
elements of
as
.
This function takes worst case O(n)
time because it has to swap the inserted element into place.
Array.insertIdx
and Array.insertIdxIfInBounds
are safer alternatives.
Examples:
#["tues", "thur", "sat"].insertIdx! 1 "wed" = #["tues", "wed", "thur", "sat"]
#["tues", "thur", "sat"].insertIdx! 2 "wed" = #["tues", "thur", "wed", "sat"]
#["tues", "thur", "sat"].insertIdx! 3 "wed" = #["tues", "thur", "sat", "wed"]
Equations
- as.insertIdx! i a = if h : i ≤ as.size then as.insertIdx i a h else panicWithPosWithDecl "Init.Data.Array.Basic" "Array.insertIdx!" 1904 7 "invalid index"
Instances For
Equations
Instances For
Inserts an element into an array at the specified index. The array is returned unmodified if the index is greater than the size of the array.
In other words, the new element is inserted into the array as
after the first i
elements of
as
.
This function takes worst case O(n)
time because it has to swap the inserted element into place.
Examples:
#["tues", "thur", "sat"].insertIdxIfInBounds 1 "wed" = #["tues", "wed", "thur", "sat"]
#["tues", "thur", "sat"].insertIdxIfInBounds 2 "wed" = #["tues", "thur", "wed", "sat"]
#["tues", "thur", "sat"].insertIdxIfInBounds 3 "wed" = #["tues", "thur", "sat", "wed"]
#["tues", "thur", "sat"].insertIdxIfInBounds 4 "wed" = #["tues", "thur", "sat"]
Equations
- as.insertIdxIfInBounds i a = if h : i ≤ as.size then as.insertIdx i a h else as
Instances For
Return true
if as
is a prefix of bs
, or false
otherwise.
Examples:
#[0, 1, 2].isPrefixOf #[0, 1, 2, 3] = true
#[0, 1, 2].isPrefixOf #[0, 1, 2] = true
#[0, 1, 2].isPrefixOf #[0, 1] = false
#[].isPrefixOf #[0, 1] = true
Equations
- as.isPrefixOf bs = if h : as.size ≤ bs.size then as.isPrefixOfAux bs h 0 else false
Instances For
Applies a function to the corresponding elements of two arrays, stopping at the end of the shorter array.
Examples:
#[1, 2].zipWith (· + ·) #[5, 6] = #[6, 8]
#[1, 2, 3].zipWith (· + ·) #[5, 6, 10] = #[6, 8, 13]
#[].zipWith (· + ·) #[5, 6] = #[]
#[x₁, x₂, x₃].zipWith f #[y₁, y₂, y₃, y₄] = #[f x₁ y₁, f x₂ y₂, f x₃ y₃]
Equations
- Array.zipWith f as bs = as.zipWithAux bs f 0 #[]
Instances For
Combines two arrays into an array of pairs in which the first and second components are the corresponding elements of each input array. The resulting array is the length of the shorter of the input arrays.
Examples:
#["Mon", "Tue", "Wed"].zip #[1, 2, 3] = #[("Mon", 1), ("Tue", 2), ("Wed", 3)]
#["Mon", "Tue", "Wed"].zip #[1, 2] = #[("Mon", 1), ("Tue", 2)]
#[x₁, x₂, x₃].zip #[y₁, y₂, y₃, y₄] = #[(x₁, y₁), (x₂, y₂), (x₃, y₃)]
Equations
- as.zip bs = Array.zipWith Prod.mk as bs
Instances For
Applies a function to the corresponding elements of both arrays, stopping when there are no more
elements in either array. If one array is shorter than the other, the function is passed none
for
the missing elements.
Examples:
#[1, 6].zipWithAll min #[5, 2] = #[some 1, some 2]
#[1, 2, 3].zipWithAll Prod.mk #[5, 6] = #[(some 1, some 5), (some 2, some 6), (some 3, none)]
#[x₁, x₂].zipWithAll f #[y] = #[f (some x₁) (some y), f (some x₂) none]
Equations
- Array.zipWithAll f as bs = Array.zipWithAll.go f as bs 0 #[]
Instances For
Separates an array of pairs into two arrays that contain the respective first and second components.
Examples:
#[("Monday", 1), ("Tuesday", 2)].unzip = (#["Monday", "Tuesday"], #[1, 2])
#[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = (#[x₁, x₂, x₃], #[y₁, y₂, y₃])
(#[] : Array (Nat × String)).unzip = ((#[], #[]) : List Nat × List String)
Equations
Instances For
Equations
Instances For
Replaces the first occurrence of a
with b
in an array. The modification is performed in-place
when the reference to the array is unique. Returns the array unmodified when a
is not present.
Examples:
#[1, 2, 3, 2, 1].replace 2 5 = #[1, 5, 3, 2, 1]
#[1, 2, 3, 2, 1].replace 0 5 = #[1, 2, 3, 2, 1]
#[].replace 2 5 = #[]
Instances For
Lexicographic ordering #
Auxiliary functions used in metaprogramming. #
We do not currently intend to provide verification theorems for these functions.
leftpad and rightpad #
Pads xs : Array α
on the left with repeated occurrences of a : α
until it is of size n
. If xs
already has at least n
elements, it is returned unmodified.
Examples:
#[1, 2, 3].leftpad 5 0 = #[0, 0, 1, 2, 3]
#["red", "green", "blue"].leftpad 4 "blank" = #["blank", "red", "green", "blue"]
#["red", "green", "blue"].leftpad 3 "blank" = #["red", "green", "blue"]
#["red", "green", "blue"].leftpad 1 "blank" = #["red", "green", "blue"]
Equations
- Array.leftpad n a xs = Array.replicate (n - xs.size) a ++ xs
Instances For
Pads xs : Array α
on the right with repeated occurrences of a : α
until it is of length n
. If
l
already has at least n
elements, it is returned unmodified.
Examples:
#[1, 2, 3].rightpad 5 0 = #[1, 2, 3, 0, 0]
#["red", "green", "blue"].rightpad 4 "blank" = #["red", "green", "blue", "blank"]
#["red", "green", "blue"].rightpad 3 "blank" = #["red", "green", "blue"]
#["red", "green", "blue"].rightpad 1 "blank" = #["red", "green", "blue"]
Equations
- Array.rightpad n a xs = xs ++ Array.replicate (n - xs.size) a
Instances For
Drop none
s from a Array, and replace each remaining some a
with a
.
Equations
- as.reduceOption = Array.filterMap id as
Instances For
eraseReps #
allDiff #
getEvenElems #
Returns a new array that contains the elements at even indices in as
, starting with the element at
index 0
.
Examples:
#[0, 1, 2, 3, 4].getEvenElems = #[0, 2, 4]
#[1, 2, 3, 4].getEvenElems = #[1, 3]
#["red", "green", "blue"].getEvenElems = #["red", "blue"]
(#[] : Array String).getEvenElems = #[]
Equations
- One or more equations did not get rendered due to their size.