Tail recursive implementations for definitions from core #
Auxiliary for setTR
: setTR.go l a xs n acc = acc.toList ++ set xs a
,
unless n ≥ l.length
in which case it returns l
Equations
- List.setTR.go l a [] x x = l
- List.setTR.go l a (head :: xs) 0 x = Array.toListAppend x (a :: xs)
- List.setTR.go l a (x_3 :: xs) (Nat.succ n) x = List.setTR.go l a xs n (Array.push x x_3)
Instances For
Auxiliary for eraseTR
: eraseTR.go l a xs acc = acc.toList ++ erase xs a
,
unless a
is not present in which case it returns l
Equations
- List.eraseTR.go l a [] x = l
- List.eraseTR.go l a (x_2 :: xs) x = bif x_2 == a then Array.toListAppend x xs else List.eraseTR.go l a xs (Array.push x x_2)
Instances For
Auxiliary for eraseIdxTR
: eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a
,
unless a
is not present in which case it returns l
Equations
- List.eraseIdxTR.go l [] x x = l
- List.eraseIdxTR.go l (head :: xs) 0 x = Array.toListAppend x xs
- List.eraseIdxTR.go l (x_3 :: xs) (Nat.succ n) x = List.eraseIdxTR.go l xs n (Array.push x x_3)
Instances For
Auxiliary for bind
: bind.go f as = acc.toList ++ bind f as
Equations
- List.bindTR.go f [] x = Array.toList x
- List.bindTR.go f (x_2 :: xs) x = List.bindTR.go f xs (x ++ f x_2)
Instances For
Auxiliary for filterMap
: filterMap.go f l = acc.toList ++ filterMap f l
Equations
- List.filterMapTR.go f [] x = Array.toList x
- List.filterMapTR.go f (x_2 :: xs) x = match f x_2 with | none => List.filterMapTR.go f xs x | some b => List.filterMapTR.go f xs (Array.push x b)
Instances For
Auxiliary for replace
: replace.go l b c xs acc = acc.toList ++ replace xs b c
,
unless b
is not found in xs
in which case it returns l
.
Equations
- List.replaceTR.go l b c [] x = l
- List.replaceTR.go l b c (x_2 :: xs) x = bif x_2 == b then Array.toListAppend x (c :: xs) else List.replaceTR.go l b c xs (Array.push x x_2)
Instances For
Auxiliary for take
: take.go l xs n acc = acc.toList ++ take n xs
,
unless n ≥ xs.length
in which case it returns l
.
Equations
- List.takeTR.go l [] x x = l
- List.takeTR.go l (head :: xs) 0 x = Array.toList x
- List.takeTR.go l (x_3 :: xs) (Nat.succ n) x = List.takeTR.go l xs n (Array.push x x_3)
Instances For
Auxiliary for takeWhile
: takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs
,
unless no element satisfying p
is found in xs
in which case it returns l
.
Equations
- List.takeWhileTR.go p l [] x = l
- List.takeWhileTR.go p l (x_2 :: xs) x = bif p x_2 then List.takeWhileTR.go p l xs (Array.push x x_2) else Array.toList x
Instances For
Tail recursive version of foldr
.
Instances For
Auxiliary for zipWith
: zipWith.go f as bs acc = acc.toList ++ zipWith f as bs
Equations
- List.zipWithTR.go f (a :: as) (b :: bs) x = List.zipWithTR.go f as bs (Array.push x (f a b))
- List.zipWithTR.go f x x x = Array.toList x
Instances For
Tail recursive version of dropLast
.
Instances For
Tail recursive version of intersperse
.
Instances For
Auxiliary for intercalateTR
:
intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)
Equations
- List.intercalateTR.go sep x [] x = Array.toListAppend x x
- List.intercalateTR.go sep x (y :: xs) x = List.intercalateTR.go sep y xs (x ++ x ++ sep)
Instances For
New definitions #
Equations
- One or more equations did not get rendered due to their size.
- List.decidableBAll p [] = isTrue fun a a_1 => List.decidableBAll.match_1 (fun a a_2 => p a) a a_1
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
- List.bagInter [] x = []
- List.bagInter x [] = []
- List.bagInter (a :: l₁) x = if List.elem a x = true then a :: List.bagInter l₁ (List.erase x a) else List.bagInter l₁ x
Instances For
Auxiliary for mapIdx
:
mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]
Equations
- List.mapIdx.go f [] x = Array.toList x
- List.mapIdx.go f (x_2 :: xs) x = List.mapIdx.go f xs (Array.push x (f (Array.size x) x_2))
Instances For
Auxiliary for mapIdxM
:
mapIdxM.go as f acc = acc.toList ++ [← f acc.size a₀, ← f (acc.size + 1) a₁, ...]
Equations
- List.mapIdxM.go f [] x = pure (Array.toList x)
- List.mapIdxM.go f (x_2 :: xs) x = do let __do_lift ← f (Array.size x) x_2 List.mapIdxM.go f xs (Array.push x __do_lift)
Instances For
after p xs
is the suffix of xs
after the first element that satisfies
p
, not including that element.
after (· == 1) [0, 1, 2, 3] = [2, 3]
drop_while (· != 1) [0, 1, 2, 3] = [1, 2, 3]
Equations
- List.after p [] = []
- List.after p (x_1 :: xs) = bif p x_1 then xs else List.after p xs
Instances For
Auxiliary for findIdx
: findIdx.go p l n = findIdx p l + n
Equations
- List.findIdx.go p [] x = x
- List.findIdx.go p (a :: l) x = bif p a then x else List.findIdx.go p l (x + 1)
Instances For
Removes the n
th element of l
, or the original list if n
is out of bounds.
Equations
- List.removeNth [] x = []
- List.removeNth (head :: xs) 0 = xs
- List.removeNth (x_2 :: xs) (Nat.succ i) = x_2 :: List.removeNth xs i
Instances For
Auxiliary for removeNthTR
:
removeNthTR.go l xs n acc = acc.toList ++ removeNth xs n
if n < length xs
, else l
.
Equations
- List.removeNthTR.go l [] x x = l
- List.removeNthTR.go l (head :: xs) 0 x = Array.toListAppend x xs
- List.removeNthTR.go l (x_3 :: xs) (Nat.succ n) x = List.removeNthTR.go l xs n (Array.push x x_3)
Instances For
Replaces the first element of the list for which f
returns some
with the returned value.
Equations
- List.replaceF f [] = []
- List.replaceF f (x_1 :: xs) = match f x_1 with | none => x_1 :: List.replaceF f xs | some a => a :: xs
Instances For
Auxiliary for replaceFTR
: replaceFTR.go f xs acc = acc.toList ++ replaceF f xs
.
Equations
- List.replaceFTR.go f [] x = Array.toList x
- List.replaceFTR.go f (x_2 :: xs) x = match f x_2 with | none => List.replaceFTR.go f xs (Array.push x x_2) | some a' => Array.toListAppend x (a' :: xs)
Instances For
Inserts an element into a list without duplication.
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).
Instances For
- slnil: ∀ {α : Type u_1}, List.Sublist [] []
the base case:
[]
is a sublist of[]
- cons: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), List.Sublist l₁ l₂ → List.Sublist l₁ (a :: l₂)
If
l₁
is a subsequence ofl₂
, then it is also a subsequence ofa :: l₂
. - cons₂: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), List.Sublist l₁ l₂ → List.Sublist (a :: l₁) (a :: l₂)
If
l₁
is a subsequence ofl₂
, thena :: l₁
is a subsequence ofa :: l₂
.
l₁ <+ l₂
, or Sublist l₁ l₂
, says that l₁
is a (non-contiguous) subsequence of l₂
.
Instances For
l₁ <+ l₂
, or Sublist l₁ l₂
, says that l₁
is a (non-contiguous) subsequence of l₂
.
Instances For
True if the first list is a potentially non-contiguous sub-sequence of the second list.
Equations
- List.isSublist [] x = true
- List.isSublist x [] = false
- List.isSublist (hd₁ :: tl₁) (hd₂ :: tl₂) = if hd₁ = hd₂ then List.isSublist tl₁ tl₂ else List.isSublist (hd₁ :: tl₁) tl₂
Instances For
Auxiliary for splitAt
: splitAt.go l n xs acc = (acc.toList ++ take n xs, drop n xs)
if n < length xs
, else (l, [])
.
Equations
- List.splitAt.go l [] x x = (l, [])
- List.splitAt.go l (x_3 :: xs) (Nat.succ n) x = List.splitAt.go l xs n (Array.push x x_3)
- List.splitAt.go l x x x = (Array.toList x, x)
Instances For
Auxiliary for splitAtD
: splitAtD.go dflt n l acc = (acc.toList ++ left, right)
if splitAtD n l dflt = (left, right)
.
Equations
- List.splitAtD.go dflt (Nat.succ n) (x_3 :: xs) x = List.splitAtD.go dflt n xs (Array.push x x_3)
- List.splitAtD.go dflt 0 x x = (Array.toList x, x)
- List.splitAtD.go dflt x [] x = (Array.toListAppend x (List.replicate x dflt), [])
Instances For
Auxiliary for splitOnP
: splitOnP.go xs acc = res'
where res'
is obtained from splitOnP P xs
by prepending acc.reverse
to the first element.
Equations
- List.splitOnP.go P [] x = [List.reverse x]
- List.splitOnP.go P (a :: t) x = if P a = true then List.reverse x :: List.splitOnP.go P t [] else List.splitOnP.go P t (a :: x)
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
- List.splitOnPTR.go P [] x x = Array.toListAppend x [Array.toList x]
- List.splitOnPTR.go P (a :: t) x x = bif P a then List.splitOnPTR.go P t #[] (Array.push x (Array.toList x)) else List.splitOnPTR.go P t (Array.push x a) x
Instances For
Apply a function to the nth tail of l
. Returns the input without
using f
if the index is larger than the length of the List.
modifyNthTail f 2 [a, b, c] = [a, b] ++ f [c]
Equations
- List.modifyNthTail f 0 x = f x
- List.modifyNthTail f (Nat.succ n) [] = []
- List.modifyNthTail f (Nat.succ n) (a :: l) = a :: List.modifyNthTail f n l
Instances For
Apply f
to the head of the list, if it exists.
Instances For
Auxiliary for modifyNthTR
: modifyNthTR.go f l n acc = acc.toList ++ modifyNth f n l
.
Equations
- List.modifyNthTR.go f [] x x = Array.toList x
- List.modifyNthTR.go f (head :: xs) 0 x = Array.toListAppend x (f head :: xs)
- List.modifyNthTR.go f (x_3 :: xs) (Nat.succ n) x = List.modifyNthTR.go f xs n (Array.push x x_3)
Instances For
Apply f
to the last element of l
, if it exists.
Instances For
Auxiliary for modifyLast
: modifyLast.go f l acc = acc.toList ++ modifyLast f l
.
Equations
- List.modifyLast.go f [] x = []
- List.modifyLast.go f [x_2] x = Array.toListAppend x [f x_2]
- List.modifyLast.go f (x_2 :: xs) x = List.modifyLast.go f xs (Array.push x x_2)
Instances For
Auxiliary for insertNthTR
: insertNthTR.go a n l acc = acc.toList ++ insertNth n a l
.
Equations
- List.insertNthTR.go a 0 x x = Array.toListAppend x (a :: x)
- List.insertNthTR.go a x [] x = Array.toList x
- List.insertNthTR.go a (Nat.succ n) (a_1 :: l) x = List.insertNthTR.go a n l (Array.push x a_1)
Instances For
Take n
elements from a list l
. If l
has less than n
elements, append n - length l
elements x
.
Equations
- List.takeD 0 x x = []
- List.takeD (Nat.succ n) x x = List.headD x x :: List.takeD n (List.tail x) x
Instances For
Auxiliary for takeDTR
: takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt
.
Equations
- List.takeDTR.go dflt (Nat.succ n) (x_3 :: xs) x = List.takeDTR.go dflt n xs (Array.push x x_3)
- List.takeDTR.go dflt 0 x x = Array.toList x
- List.takeDTR.go dflt x [] x = Array.toListAppend x (List.replicate x dflt)
Instances For
Fold a function f
over the list from the left, returning the list of partial results.
scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
Equations
- List.scanl f a [] = [a]
- List.scanl f a (x_1 :: xs) = a :: List.scanl f (f a x_1) xs
Instances For
Auxiliary for scanlTR
: scanlTR.go f l a acc = acc.toList ++ scanl f a l
.
Equations
- List.scanlTR.go f [] x x = Array.toListAppend x [x]
- List.scanlTR.go f (b :: l) x x = List.scanlTR.go f l (f x b) (Array.push x x)
Instances For
Given a function f : α → β ⊕ γ
, partitionMap f l
maps the list by f
whilst partitioning the result it into a pair of lists, List β × List γ
,
partitioning the .inl _
into the left list, and the .inr _
into the right List.
partitionMap (id : Nat ⊕ Nat → Nat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
Instances For
Auxiliary for partitionMap
:
partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right)
if partitionMap f l = (left, right)
.
Equations
- List.partitionMap.go f [] x x = (Array.toList x, Array.toList x)
- List.partitionMap.go f (x_3 :: xs) x x = match f x_3 with | Sum.inl a => List.partitionMap.go f xs (Array.push x a) x | Sum.inr b => List.partitionMap.go f xs x (Array.push x b)
Instances For
Auxiliary for partitionM
:
partitionM.go p l acc₁ acc₂
returns (acc₁.toList ++ left, acc₂.toList ++ right)
if partitionM p l
returns (left, right)
.
Equations
- List.partitionM.go p [] x x = pure (Array.toList x, Array.toList x)
- List.partitionM.go p (x_3 :: xs) x x = do let __do_lift ← p x_3 if __do_lift = true then List.partitionM.go p xs (Array.push x x_3) x else List.partitionM.go p xs x (Array.push x x_3)
Instances For
Fold a list from left to right as with foldl
, but the combining function
also receives each element's index.
Equations
- List.foldlIdx f init [] x = init
- List.foldlIdx f init (b :: l) x = List.foldlIdx f (f x init b) l (x + 1)
Instances For
Fold a list from right to left as with foldr
, but the combining function
also receives each element's index.
Equations
- List.foldrIdx f init [] x = init
- List.foldrIdx f init (b :: l) x = f x b (List.foldrIdx f init l (x + 1))
Instances For
Return the index of the first occurrence of an element satisfying p
.
Equations
- List.findIdx? p [] x = none
- List.findIdx? p (b :: l) x = if p b = true then some x else List.findIdx? p l (x + 1)
Instances For
Partial map. If f : Π a, p a → β
is a partial function defined on
a : α
satisfying p
, then pmap f l h
is essentially the same as map f l
but is defined only when all members of l
satisfy p
, using the proof
to apply f
.
Equations
Instances For
Auxiliary for lookmap
: lookmap.go f l acc = acc.toList ++ lookmap f l
.
Equations
- List.lookmap.go f [] x = Array.toList x
- List.lookmap.go f (x_2 :: xs) x = match f x_2 with | some b => Array.toListAppend x (b :: xs) | none => List.lookmap.go f xs (Array.push x x_2)
Instances For
Auxiliary for countP
: countP.go p l acc = countP p l + acc
.
Equations
- List.countP.go p [] x = x
- List.countP.go p (a :: l) x = bif p a then List.countP.go p l (x + 1) else List.countP.go p l x
Instances For
isPrefix l₁ l₂
, or l₁ <+: l₂
, means that l₁
is a prefix of l₂
,
that is, l₂
has the form l₁ ++ t
for some t
.
Instances For
isSuffix l₁ l₂
, or l₁ <:+ l₂
, means that l₁
is a suffix of l₂
,
that is, l₂
has the form t ++ l₁
for some t
.
Instances For
isInfix l₁ l₂
, or l₁ <:+: l₂
, means that l₁
is a contiguous
substring of l₂
, that is, l₂
has the form s ++ l₁ ++ t
for some s, t
.
Instances For
inits l
is the list of initial segments of l
.
inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]
Equations
- List.inits [] = [[]]
- List.inits (x_1 :: xs) = [] :: List.map (fun t => x_1 :: t) (List.inits xs)
Instances For
tails l
is the list of terminal segments of l
.
tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]
Equations
- List.tails [] = [[]]
- List.tails (x_1 :: xs) = (x_1 :: xs) :: List.tails xs
Instances For
Auxiliary for tailsTR
: tailsTR.go l acc = acc.toList ++ tails l
.
Equations
- List.tailsTR.go [] acc = Array.toListAppend acc [[]]
- List.tailsTR.go (x_1 :: xs) acc = List.tailsTR.go xs (Array.push acc (x_1 :: xs))
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]]
Instances For
- nil: ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, List.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 → List.Forall₂ R l₁ l₂ → List.Forall₂ R (a :: l₁) (b :: l₂)
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.
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]]
Instances For
List of all sections through a list of lists. A section
of [L₁, L₂, ..., Lₙ]
is a list whose first element comes from
L₁
, whose second element comes from L₂
, and so on.
Equations
- List.sections [] = [[]]
- List.sections (l :: L) = List.bind (List.sections L) fun s => List.map (fun a => a :: s) l
Instances For
eraseP p l
removes the first element of l
satisfying the predicate p
.
Equations
- List.eraseP p [] = []
- List.eraseP p (x_1 :: xs) = bif p x_1 then xs else x_1 :: List.eraseP p xs
Instances For
Auxiliary for erasePTR
: erasePTR.go p l xs acc = acc.toList ++ eraseP p xs
,
unless xs
does not contain any elements satisfying p
, where it returns l
.
Equations
- List.erasePTR.go p l [] x = l
- List.erasePTR.go p l (x_2 :: xs) x = bif p x_2 then Array.toListAppend x xs else List.erasePTR.go p l xs (Array.push x x_2)
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
- List.extractP.go p l [] x = (none, l)
- List.extractP.go p l (x_2 :: xs) x = bif p x_2 then (some x_2, Array.toListAppend x xs) else List.extractP.go p l xs (Array.push x x_2)
Instances For
ofFnNthVal f i
returns some (f i)
if i < n
and none
otherwise.
Instances For
Returns the longest initial prefix of two lists such that they are pairwise related by R
.
takeWhile₂ (· < ·) [1, 2, 4, 5] [5, 4, 3, 6] = ([1, 2], [5, 4])
Equations
- List.takeWhile₂ R (a :: as) (b :: bs) = if R a b = true then match List.takeWhile₂ R as bs with | (as', bs') => (a :: as', b :: bs') else ([], [])
- List.takeWhile₂ R x x = ([], [])
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
- List.takeWhile₂TR.go R (a :: as) (b :: bs) x x = bif R a b then List.takeWhile₂TR.go R as bs (a :: x) (b :: x) else (List.reverse x, List.reverse x)
- List.takeWhile₂TR.go R x x x x = (List.reverse x, List.reverse x)
Instances For
- nil: ∀ {α : Type u_1} {R : α → α → Prop}, List.Pairwise R []
All elements of the empty list are vacuously pairwise related.
- cons: ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α}, (∀ (a' : α), a' ∈ l → R a a') → List.Pairwise R l → List.Pairwise R (a :: l)
Pairwise R l
means that all the elements with earlier indexes are
R
-related to all the elements with later indexes.
Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
For example if R = (·≠·)
then it asserts l
has no duplicates,
and if R = (·<·)
then it asserts that l
is (strictly) sorted.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- List.instDecidablePairwise [] = isTrue (_ : List.Pairwise R [])
- nil: ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.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 → List.Chain R b l → List.Chain R a (b :: l)
If
a
relates tob
andb::l
is a chain, thena :: b :: l
is also a chain.
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
Instances For
range' start len step
is the list of numbers [start, start+step, ..., start+(len-1)*step]
.
It is intended mainly for proving properties of range
and iota
.
Equations
- List.range' x 0 x = []
- List.range' x (Nat.succ n) x = x :: List.range' (x + x) n x
Instances For
Auxiliary for range'TR
: range'TR.go n e = [e-n, ..., e-1] ++ acc
.
Equations
- List.range'TR.go step 0 x x = x
- List.range'TR.go step (Nat.succ n) x x = List.range'TR.go step n (x - step) ((x - step) :: x)
Instances For
ilast' x xs
returns the last element of xs
if xs
is non-empty; it returns x
otherwise.
Equations
- List.ilast' x [] = x
- List.ilast' x (b :: l) = List.ilast' b l
Instances For
last' xs
returns the last element of xs
if xs
is non-empty; it returns none
otherwise.
Equations
- List.last' [] = none
- List.last' [a] = some a
- List.last' (head :: l) = List.last' l
Instances For
rotate'
is the same as rotate
, but slower. Used for proofs about rotate
Equations
- List.rotate' [] x = []
- List.rotate' x 0 = x
- List.rotate' (a :: l) (Nat.succ n) = List.rotate' (l ++ [a]) n
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]
Instances For
Auxiliary for mapDiagM
: mapDiagM.go as f acc = (acc.toList ++ ·) <$> mapDiagM f as
Equations
- List.mapDiagM.go f [] x = pure (Array.toList x)
- List.mapDiagM.go f (x_2 :: xs) x = do let b ← f x_2 x_2 let acc ← List.foldlM (fun x x_1 => Array.push x <$> f x_2 x_1) (Array.push x b) xs List.mapDiagM.go f xs acc
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
- List.forDiagM f [] = pure PUnit.unit
- List.forDiagM f (x_1 :: xs) = do f x_1 x_1 List.forM xs (f x_1) List.forDiagM f xs
Instances For
getRest l l₁
returns some l₂
if l = l₁ ++ l₂
.
If l₁
is not a prefix of l
, returns none
Equations
- List.getRest x [] = some x
- List.getRest [] x = none
- List.getRest (x_2 :: l) (y :: l₁) = if x_2 = y then List.getRest l l₁ else none
Instances For
List.dropSlice n m xs
removes a slice of length m
at index n
in list xs
.
Equations
- List.dropSlice x x [] = []
- List.dropSlice 0 x x = List.drop x x
- List.dropSlice (Nat.succ n) x (x_3 :: xs) = x_3 :: List.dropSlice n x xs
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
- List.dropSliceTR.go l m [] x x = l
- List.dropSliceTR.go l m (head :: xs) 0 x = Array.toListAppend x (List.drop m xs)
- List.dropSliceTR.go l m (x_3 :: xs) (Nat.succ n) x = List.dropSliceTR.go l m xs n (Array.push x x_3)
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
- List.zipWithLeft' f [] x = ([], x)
- List.zipWithLeft' f (a :: as) [] = (List.map (fun a => f a none) (a :: as), [])
- List.zipWithLeft' f (a :: as) (b :: bs) = let r := List.zipWithLeft' f as bs; (f a (some b) :: r.fst, r.snd)
Instances For
Auxiliary for zipWithLeft'TR
: zipWithLeft'TR.go l acc = acc.toList ++ zipWithLeft' l
.
Equations
- List.zipWithLeft'TR.go f [] x x = (Array.toList x, x)
- List.zipWithLeft'TR.go f x [] x = (Array.toList (List.foldl (fun acc a => Array.push acc (f a none)) x x), [])
- List.zipWithLeft'TR.go f (a :: as) (b :: bs) x = List.zipWithLeft'TR.go f as bs (Array.push x (f a (some b)))
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])
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
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
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
- List.zipWithLeft f [] x = []
- List.zipWithLeft f (a :: as) [] = List.map (fun a => f a none) (a :: as)
- List.zipWithLeft f (a :: as) (b :: bs) = f a (some b) :: List.zipWithLeft f as bs
Instances For
Tail-recursive version of zipWithLeft
.
Instances For
Auxiliary for zipWithLeftTR
: zipWithLeftTR.go l acc = acc.toList ++ zipWithLeft l
.
Equations
- List.zipWithLeftTR.go f [] x x = Array.toList x
- List.zipWithLeftTR.go f x [] x = Array.toList (List.foldl (fun acc a => Array.push acc (f a none)) x x)
- List.zipWithLeftTR.go f (a :: as) (b :: bs) x = List.zipWithLeftTR.go f as bs (Array.push x (f a (some b)))
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
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
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
Instances For
fillNones xs ys
replaces the none
s in xs
with elements of ys
. If there
are not enough ys
to replace all the none
s, the remaining none
s are
dropped from xs
.
fillNones [none, some 1, none, none] [2, 3] = [2, 1, 3]
Equations
- List.fillNones [] x = []
- List.fillNones (some a :: as) x = a :: List.fillNones as x
- List.fillNones (none :: as) [] = List.reduceOption as
- List.fillNones (none :: as) (a :: as') = a :: List.fillNones as as'
Instances For
Auxiliary for fillNonesTR
: fillNonesTR.go as as' acc = acc.toList ++ fillNones as as'
.
Equations
- List.fillNonesTR.go [] x x = Array.toList x
- List.fillNonesTR.go (some a :: as) x x = List.fillNonesTR.go as x (Array.push x a)
- List.fillNonesTR.go (none :: as) [] x = List.filterMapTR.go id as x
- List.fillNonesTR.go (none :: as) (a :: as') x = List.fillNonesTR.go as as' (Array.push x a)
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
- List.takeList x [] = ([], x)
- List.takeList x (n :: ns) = match List.splitAt n x with | (xs₁, xs₂) => match List.takeList xs₂ ns with | (xss, rest) => (xs₁ :: xss, rest)
Instances For
Auxiliary for takeListTR
: takeListTR.go as as' acc = acc.toList ++ takeList as as'
.
Equations
- List.takeListTR.go [] x x = (Array.toList x, x)
- List.takeListTR.go (n :: ns) x x = match List.splitAt n x with | (xs₁, xs₂) => List.takeListTR.go ns xs₂ (Array.push x xs₁)
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
- List.toChunksAux n [] x = ([], [])
- List.toChunksAux n (head :: xs) 0 = match List.toChunksAux n xs n with | (l, L) => ([], (head :: l) :: L)
- List.toChunksAux n (x_2 :: xs) (Nat.succ i) = match List.toChunksAux n xs i with | (l, L) => (x_2 :: l, L)
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]]
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
- One or more equations did not get rendered due to their size.
- List.toChunks.go n [] x x = Array.toList (Array.push x (Array.toList x))
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
.
Ternary version of List.zipWith
.
Equations
- List.zipWith₃ f (x_3 :: xs) (y :: ys) (z :: zs) = f x_3 y z :: List.zipWith₃ f xs ys zs
- List.zipWith₃ f x x x = []
Instances For
Quaternary version of List.zipWith
.
Equations
- List.zipWith₄ f (x_4 :: xs) (y :: ys) (z :: zs) (u :: us) = f x_4 y z u :: List.zipWith₄ f xs ys zs us
- List.zipWith₄ f x x x x = []
Instances For
Quinary version of List.zipWith
.
Equations
- List.zipWith₅ f (x_5 :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) = f x_5 y z u v :: List.zipWith₅ f xs ys zs us vs
- List.zipWith₅ f x x x x x = []
Instances For
An auxiliary function for List.mapWithPrefixSuffix
.
Equations
- List.mapWithPrefixSuffixAux f x [] = []
- List.mapWithPrefixSuffixAux f x (a :: l₂) = f x a l₂ :: List.mapWithPrefixSuffixAux f (List.concat x a) l₂
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 []]
.
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]]
.