New definitions #
Computes the "bag intersection" of l₁
and l₂
, that is,
the collection of elements of l₁
which are also in l₂
. As each element
is identified, it is removed from l₂
, so elements are counted with multiplicity.
Equations
Instances For
Auxiliary for replaceFTR
: replaceFTR.go f xs acc = acc.toList ++ replaceF f xs
.
Equations
Instances For
Constructs the union of two lists, by inserting the elements of l₁
in reverse order to l₂
.
As a result, l₂
will always be a suffix, but only the last occurrence of each element in l₁
will be retained (but order will otherwise be preserved).
Equations
Instances For
Auxiliary for splitOnP
: splitOnP.go xs acc r = r.toList ++ res'
where res'
is obtained from splitOnP P xs
by prepending acc.toList
to the first element.
Equations
Instances For
Apply f
to the last element of l
, if it exists.
Equations
Instances For
Auxiliary for modifyLast
: modifyLast.go f l acc = acc.toList ++ modifyLast f l
.
Equations
Instances For
Auxiliary for takeDTR
: takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt
.
Equations
Instances For
Auxiliary for scanlTR
: scanlTR.go f l a acc = acc.toList ++ scanl f a l
.
Equations
Instances For
Auxiliary for lookmap
: lookmap.go f l acc = acc.toList ++ lookmap f l
.
Equations
Instances For
sublists' l
is the list of all (non-contiguous) sublists of l
.
It differs from sublists
only in the order of appearance of the sublists;
sublists'
uses the first element of the list as the MSB,
sublists
uses the first element of the list as the LSB.
sublists' [1, 2, 3] = [[], [3], [2], [2, 3], [1], [1, 3], [1, 2], [1, 2, 3]]
Equations
Instances For
A version of List.sublists
that has faster runtime performance but worse kernel performance
Equations
Instances For
Forall₂ R l₁ l₂
means that l₁
and l₂
have the same length,
and whenever a
is the nth element of l₁
, and b
is the nth element of l₂
,
then R a b
is satisfied.
- nil
{α : Type u_1}
{β : Type u_2}
{R : α → β → Prop}
: Forall₂ R [] []
Two nil lists are
Forall₂
-related - cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β} : R a b → Forall₂ R l₁ l₂ → Forall₂ R (a :: l₁) (b :: l₂)
Instances For
go : List α → Array (List α) → Array (List α)
handles the insertion of
a new list into all the lists in the array:
go [a, b, c] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃]
.
If the new list is too short, the later lists are unchanged, and if it is too long
the array is extended:
go [a] #[l₁, l₂, l₃] = #[a::l₁, l₂, l₃]
go [a, b, c, d] #[l₁, l₂, l₃] = #[a::l₁, b::l₂, c::l₃, [d]]
Equations
Instances For
Auxiliary for extractP
:
extractP.go p l xs acc = (some a, acc.toList ++ out)
if extractP p xs = (some a, out)
,
and extractP.go p l xs acc = (none, l)
if extractP p xs = (none, _)
.
Equations
Instances For
Auxiliary for takeWhile₂TR
:
takeWhile₂TR.go R as bs acca accb = (acca.reverse ++ as', acca.reverse ++ bs')
if takeWhile₂ R as bs = (as', bs')
.
Equations
Instances For
Chain R a l
means that R
holds between adjacent elements of a::l
.
Chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d
- nil
{α : Type u_1}
{R : α → α → Prop}
{a : α}
: Chain R a []
A chain of length 1 is trivially a chain.
- cons
{α : Type u_1}
{R : α → α → Prop}
{a b : α}
{l : List α}
: R a b → Chain R b l → Chain R a (b :: l)
If
a
relates tob
andb::l
is a chain, thena :: b :: l
is also a chain.
Instances For
mapDiagM f l
calls f
on all elements in the upper triangular part of l × l
.
That is, for each e ∈ l
, it will run f e e
and then f e e'
for each e'
that appears after e
in l
.
mapDiagM f [1, 2, 3] =
return [← f 1 1, ← f 1 2, ← f 1 3, ← f 2 2, ← f 2 3, ← f 3 3]
Equations
Instances For
forDiagM f l
calls f
on all elements in the upper triangular part of l × l
.
That is, for each e ∈ l
, it will run f e e
and then f e e'
for each e'
that appears after e
in l
.
forDiagM f [1, 2, 3] = do f 1 1; f 1 2; f 1 3; f 2 2; f 2 3; f 3 3
Equations
Instances For
getRest l l₁
returns some l₂
if l = l₁ ++ l₂
.
If l₁
is not a prefix of l
, returns none
Equations
Instances For
Auxiliary for dropSliceTR
: dropSliceTR.go l m xs n acc = acc.toList ++ dropSlice n m xs
unless n ≥ length xs
, in which case it is l
.
Equations
Instances For
Left-biased version of List.zipWith
. zipWithLeft' f as bs
applies f
to each
pair of elements aᵢ ∈ as
and bᵢ ∈ bs
. If bs
is shorter than as
, f
is
applied to none
for the remaining aᵢ
. Returns the results of the f
applications and the remaining bs
.
zipWithLeft' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipWithLeft' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
Equations
Instances For
Auxiliary for zipWithLeft'TR
: zipWithLeft'TR.go l acc = acc.toList ++ zipWithLeft' l
.
Equations
Instances For
Right-biased version of List.zipWith
. zipWithRight' f as bs
applies f
to each
pair of elements aᵢ ∈ as
and bᵢ ∈ bs
. If as
is shorter than bs
, f
is
applied to none
for the remaining bᵢ
. Returns the results of the f
applications and the remaining as
.
zipWithRight' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipWithRight' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
Equations
Instances For
Left-biased version of List.zip
. zipLeft' as bs
returns the list of
pairs (aᵢ, bᵢ)
for aᵢ ∈ as
and bᵢ ∈ bs
. If bs
is shorter than as
, the
remaining aᵢ
are paired with none
. Also returns the remaining bs
.
zipLeft' [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipLeft' [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
zipLeft' = zipWithLeft' prod.mk
Equations
Instances For
Right-biased version of List.zip
. zipRight' as bs
returns the list of
pairs (aᵢ, bᵢ)
for aᵢ ∈ as
and bᵢ ∈ bs
. If as
is shorter than bs
, the
remaining bᵢ
are paired with none
. Also returns the remaining as
.
zipRight' [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipRight' [1, 2] ['a'] = ([(some 1, 'a')], [2])
zipRight' = zipWithRight' prod.mk
Equations
Instances For
Left-biased version of List.zipWith
. zipWithLeft f as bs
applies f
to each pair
aᵢ ∈ as
and bᵢ ∈ bs∈ bs
. If bs
is shorter than as
, f
is applied to none
for the remaining aᵢ
.
zipWithLeft prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipWithLeft prod.mk [1] ['a', 'b'] = [(1, some 'a')]
zipWithLeft f as bs = (zipWithLeft' f as bs).fst
Equations
Instances For
Tail-recursive version of zipWithLeft
.
Equations
Instances For
Auxiliary for zipWithLeftTR
: zipWithLeftTR.go l acc = acc.toList ++ zipWithLeft l
.
Equations
Instances For
Right-biased version of List.zipWith
. zipWithRight f as bs
applies f
to each
pair aᵢ ∈ as
and bᵢ ∈ bs∈ bs
. If as
is shorter than bs
, f
is applied to
none
for the remaining bᵢ
.
zipWithRight prod.mk [1, 2] ['a'] = [(some 1, 'a')]
zipWithRight prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipWithRight f as bs = (zipWithRight' f as bs).fst
Equations
Instances For
Left-biased version of List.zip
. zipLeft as bs
returns the list of pairs
(aᵢ, bᵢ)
for aᵢ ∈ as
and bᵢ ∈ bs
. If bs
is shorter than as
, the
remaining aᵢ
are paired with none
.
zipLeft [1, 2] ['a'] = [(1, some 'a'), (2, none)]
zipLeft [1] ['a', 'b'] = [(1, some 'a')]
zipLeft = zipWithLeft prod.mk
Equations
Instances For
Right-biased version of List.zip
. zipRight as bs
returns the list of pairs
(aᵢ, bᵢ)
for aᵢ ∈ as
and bᵢ ∈ bs
. If as
is shorter than bs
, the
remaining bᵢ
are paired with none
.
zipRight [1, 2] ['a'] = [(some 1, 'a')]
zipRight [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
zipRight = zipWithRight prod.mk
Equations
Instances For
Auxiliary for fillNonesTR
: fillNonesTR.go as as' acc = acc.toList ++ fillNones as as'
.
Equations
Instances For
takeList as ns
extracts successive sublists from as
. For ns = n₁ ... nₘ
,
it first takes the n₁
initial elements from as
, then the next n₂
ones,
etc. It returns the sublists of as
-- one for each nᵢ
-- and the remaining
elements of as
. If as
does not have at least as many elements as the sum of
the nᵢ
, the corresponding sublists will have less than nᵢ
elements.
takeList ['a', 'b', 'c', 'd', 'e'] [2, 1, 1] = ([['a', 'b'], ['c'], ['d']], ['e'])
takeList ['a', 'b'] [3, 1] = ([['a', 'b'], []], [])
Equations
Instances For
Auxiliary for takeListTR
: takeListTR.go as as' acc = acc.toList ++ takeList as as'
.
Equations
Instances For
Auxliary definition used to define toChunks
.
toChunksAux n xs i
returns (xs.take i, (xs.drop i).toChunks (n+1))
,
that is, the first i
elements of xs
, and the remaining elements chunked into
sublists of length n+1
.
Equations
Instances For
xs.toChunks n
splits the list into sublists of size at most n
,
such that (xs.toChunks n).join = xs
.
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 10 = [[1, 2, 3, 4, 5, 6, 7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 3 = [[1, 2, 3], [4, 5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 2 = [[1, 2], [3, 4], [5, 6], [7, 8]]
[1, 2, 3, 4, 5, 6, 7, 8].toChunks 0 = [[1, 2, 3, 4, 5, 6, 7, 8]]
Equations
Instances For
Auxliary definition used to define toChunks
.
toChunks.go xs acc₁ acc₂
pushes elements into acc₁
until it reaches size n
,
then it pushes the resulting list to acc₂
and continues until xs
is exhausted.
Equations
Instances For
We add some n-ary versions of List.zipWith
for functions with more than two arguments.
These can also be written in terms of List.zip
or List.zipWith
.
For example, zipWith₃ f xs ys zs
could also be written as
zipWith id (zipWith f xs ys) zs
or as
(zip xs <| zip ys zs).map fun ⟨x, y, z⟩ => f x y z
.
An auxiliary function for List.mapWithPrefixSuffix
.
Equations
Instances For
List.mapWithPrefixSuffix f l
maps f
across a list l
.
For each a ∈ l
with l = pref ++ [a] ++ suff
, a
is mapped to f pref a suff
.
Example: if f : list Nat → Nat → list Nat → β
,
List.mapWithPrefixSuffix f [1, 2, 3]
will produce the list
[f [] 1 [2, 3], f [1] 2 [3], f [1, 2] 3 []]
.
Equations
Instances For
List.mapWithComplement f l
is a variant of List.mapWithPrefixSuffix
that maps f
across a list l
.
For each a ∈ l
with l = pref ++ [a] ++ suff
, a
is mapped to f a (pref ++ suff)
,
i.e., the list input to f
is l
with a
removed.
Example: if f : Nat → list Nat → β
, List.mapWithComplement f [1, 2, 3]
will produce the list
[f 1 [2, 3], f 2 [1, 3], f 3 [1, 2]]
.
Equations
Instances For
Map each element of a List
to an action, evaluate these actions in order,
and collect the results.
Equations
Instances For
Subperm l₁ l₂
, denoted l₁ <+~ l₂
, means that l₁
is a sublist of
a permutation of l₂
. This is an analogue of l₁ ⊆ l₂
which respects
multiplicities of elements, and is used for the ≤
relation on multisets.
Equations
Instances For
O(|l₁| * (|l₁| + |l₂|))
. Computes whether l₁
is a sublist of a permutation of l₂
.
See isSubperm_iff
for a characterization in terms of List.Subperm
.
Equations
Instances For
dropPrefix? l p
returns
some r
if l = p' ++ r
for some p'
which is paiwise ==
to p
,
and none
otherwise.
Equations
Instances For
dropSuffix? l s
returns
some r
if l = r ++ s'
for some s'
which is paiwise ==
to s
,
and none
otherwise.
Equations
Instances For
dropInfix? l i
returns
some (p, s)
if l = p ++ i' ++ s
for some i'
which is paiwise ==
to i
,
and none
otherwise.
Note that this is an inefficient implementation, and if computation time is a concern you should be
using the Knuth-Morris-Pratt algorithm as implemented in Batteries.Data.List.Matcher
.