Documentation

Std.Data.List.Basic

Tail recursive implementations for definitions from core #

@[inline]
def List.setTR {α : Type u_1} (l : List α) (n : Nat) (a : α) :
List α

Tail recursive version of erase.

Equations
Instances For
    def List.setTR.go {α : Type u_1} (l : List α) (a : α) :
    List αNatArray αList α

    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
    Instances For
      theorem List.set_eq_setTR.go (α : Type u_1) (l : List α) (a : α) (acc : Array α) (xs : List α) (n : Nat) :
      l = acc.data ++ xsList.setTR.go l a xs n acc = acc.data ++ List.set xs n a
      @[inline]
      def List.eraseTR {α : Type u_1} [BEq α] (l : List α) (a : α) :
      List α

      Tail recursive version of erase.

      Equations
      Instances For
        def List.eraseTR.go {α : Type u_1} [BEq α] (l : List α) (a : α) :
        List αArray αList α

        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
        Instances For
          @[inline]
          def List.eraseIdxTR {α : Type u_1} (l : List α) (n : Nat) :
          List α

          Tail recursive version of eraseIdx.

          Equations
          Instances For
            def List.eraseIdxTR.go {α : Type u_1} (l : List α) :
            List αNatArray αList α

            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
            Instances For
              @[inline]
              def List.bindTR {α : Type u_1} {β : Type u_2} (as : List α) (f : αList β) :
              List β

              Tail recursive version of bind.

              Equations
              Instances For
                @[specialize #[]]
                def List.bindTR.go {α : Type u_1} {β : Type u_2} (f : αList β) :
                List αArray βList β

                Auxiliary for bind: bind.go f as = acc.toList ++ bind f as

                Equations
                Instances For
                  theorem List.bind_eq_bindTR.go (α : Type u_2) (β : Type u_1) (f : αList β) (as : List α) (acc : Array β) :
                  List.bindTR.go f as acc = acc.data ++ List.bind as f
                  @[inline]
                  def List.joinTR {α : Type u_1} (l : List (List α)) :
                  List α

                  Tail recursive version of join.

                  Equations
                  Instances For
                    @[inline]
                    def List.filterMapTR {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
                    List β

                    Tail recursive version of filterMap.

                    Equations
                    Instances For
                      @[specialize #[]]
                      def List.filterMapTR.go {α : Type u_1} {β : Type u_2} (f : αOption β) :
                      List αArray βList β

                      Auxiliary for filterMap: filterMap.go f l = acc.toList ++ filterMap f l

                      Equations
                      Instances For
                        theorem List.filterMap_eq_filterMapTR.go (α : Type u_2) (β : Type u_1) (f : αOption β) (as : List α) (acc : Array β) :
                        List.filterMapTR.go f as acc = acc.data ++ List.filterMap f as
                        @[inline]
                        def List.replaceTR {α : Type u_1} [BEq α] (l : List α) (b : α) (c : α) :
                        List α

                        Tail recursive version of replace.

                        Equations
                        Instances For
                          @[specialize #[]]
                          def List.replaceTR.go {α : Type u_1} [BEq α] (l : List α) (b : α) (c : α) :
                          List αArray αList α

                          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
                          Instances For
                            @[inline]
                            def List.takeTR {α : Type u_1} (n : Nat) (l : List α) :
                            List α

                            Tail recursive version of take.

                            Equations
                            Instances For
                              @[specialize #[]]
                              def List.takeTR.go {α : Type u_1} (l : List α) :
                              List αNatArray αList α

                              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
                              Instances For
                                @[inline]
                                def List.takeWhileTR {α : Type u_1} (p : αBool) (l : List α) :
                                List α

                                Tail recursive version of takeWhile.

                                Equations
                                Instances For
                                  @[specialize #[]]
                                  def List.takeWhileTR.go {α : Type u_1} (p : αBool) (l : List α) :
                                  List αArray αList α

                                  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
                                  Instances For
                                    @[specialize #[]]
                                    def List.foldrTR {α : Type u_1} {β : Type u_2} (f : αββ) (init : β) (l : List α) :
                                    β

                                    Tail recursive version of foldr.

                                    Equations
                                    Instances For
                                      @[inline]
                                      def List.zipWithTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : List α) (bs : List β) :
                                      List γ

                                      Tail recursive version of zipWith.

                                      Equations
                                      Instances For
                                        def List.zipWithTR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
                                        List αList βArray γList γ

                                        Auxiliary for zipWith: zipWith.go f as bs acc = acc.toList ++ zipWith f as bs

                                        Equations
                                        Instances For
                                          theorem List.zipWith_eq_zipWithTR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : αβγ) (as : List α) (bs : List β) (acc : Array γ) :
                                          List.zipWithTR.go f as bs acc = acc.data ++ List.zipWith f as bs
                                          def List.unzipTR {α : Type u_1} {β : Type u_2} (l : List (α × β)) :
                                          List α × List β

                                          Tail recursive version of unzip.

                                          Equations
                                          Instances For
                                            def List.enumFromTR {α : Type u_1} (n : Nat) (l : List α) :
                                            List (Nat × α)

                                            Tail recursive version of enumFrom.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem List.enumFrom_eq_enumFromTR.go (α : Type u_1) (l : List α) (n : Nat) :
                                              let f := fun a x => match x with | (n, acc) => (n - 1, (n - 1, a) :: acc); List.foldr f (n + List.length l, []) l = (n, List.enumFrom n l)
                                              theorem List.replicateTR_loop_eq :
                                              ∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), List.replicateTR.loop a n acc = List.replicate n a ++ acc
                                              @[inline]
                                              def List.dropLastTR {α : Type u_1} (l : List α) :
                                              List α

                                              Tail recursive version of dropLast.

                                              Equations
                                              Instances For
                                                def List.intersperseTR {α : Type u_1} (sep : α) :
                                                List αList α

                                                Tail recursive version of intersperse.

                                                Equations
                                                Instances For
                                                  def List.intercalateTR {α : Type u_1} (sep : List α) :
                                                  List (List α)List α

                                                  Tail recursive version of intercalate.

                                                  Equations
                                                  Instances For
                                                    def List.intercalateTR.go {α : Type u_1} (sep : Array α) :
                                                    List αList (List α)Array αList α

                                                    Auxiliary for intercalateTR: intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)

                                                    Equations
                                                    Instances For
                                                      theorem List.intercalate_eq_intercalateTR.go (α : Type u_1) (sep : List α) {acc : Array α} {x : List α} (xs : List (List α)) :
                                                      List.intercalateTR.go (List.toArray sep) x xs acc = acc.data ++ List.join (List.intersperse sep (x :: xs))

                                                      New definitions #

                                                      def List.Subset {α : Type u_1} (l₁ : List α) (l₂ : List α) :

                                                      l₁ ⊆ l₂ means that every element of l₁ is also an element of l₂, ignoring multiplicity.

                                                      Equations
                                                      Instances For
                                                        instance List.instHasSubsetList {α : Type u_1} :
                                                        Equations
                                                        • List.instHasSubsetList = { Subset := List.Subset }
                                                        instance List.decidableBEx {α : Type u_1} (p : αProp) [DecidablePred p] (l : List α) :
                                                        Decidable (x, x l p x)
                                                        Equations
                                                        instance List.decidableBAll {α : Type u_1} (p : αProp) [DecidablePred p] (l : List α) :
                                                        Decidable ((x : α) → x lp x)
                                                        Equations
                                                        def List.bagInter {α : Type u_1} [BEq α] :
                                                        List αList αList α

                                                        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
                                                          def List.diff {α : Type u_1} [BEq α] :
                                                          List αList αList α

                                                          Computes the difference of l₁ and l₂, by removing each element in l₂ from l₁.

                                                          Equations
                                                          Instances For
                                                            def List.tail {α : Type u_1} :
                                                            List αList α

                                                            Get the tail of a nonempty list, or return [] for [].

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem List.tail_nil {α : Type u_1} :
                                                              List.tail [] = []
                                                              @[simp]
                                                              theorem List.tail_cons {α : Type u_1} {a : α} {as : List α} :
                                                              List.tail (a :: as) = as
                                                              @[inline]
                                                              def List.next? {α : Type u_1} :
                                                              List αOption (α × List α)

                                                              Get the head and tail of a list, if it is nonempty.

                                                              Equations
                                                              Instances For
                                                                @[inline]
                                                                def List.mapIdx {α : Type u_1} {β : Type u_2} (f : Natαβ) (as : List α) :
                                                                List β

                                                                Given a function f : Nat → α → β and as : list α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

                                                                Equations
                                                                Instances For
                                                                  @[specialize #[]]
                                                                  def List.mapIdx.go {α : Type u_1} {β : Type u_2} (f : Natαβ) :
                                                                  List αArray βList β

                                                                  Auxiliary for mapIdx: mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]

                                                                  Equations
                                                                  Instances For
                                                                    @[inline]
                                                                    def List.mapIdxM {α : Type u_1} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (f : Natαm β) :
                                                                    m (List β)

                                                                    Monadic variant of mapIdx.

                                                                    Equations
                                                                    Instances For
                                                                      @[specialize #[]]
                                                                      def List.mapIdxM.go {α : Type u_1} {β : Type v} {m : Type v → Type w} [Monad m] (f : Natαm β) :
                                                                      List αArray βm (List β)

                                                                      Auxiliary for mapIdxM: mapIdxM.go as f acc = acc.toList ++ [← f acc.size a₀, ← f (acc.size + 1) a₁, ...]

                                                                      Equations
                                                                      Instances For
                                                                        @[specialize #[]]
                                                                        def List.after {α : Type u_1} (p : αBool) :
                                                                        List αList α

                                                                        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
                                                                        Instances For
                                                                          @[inline]
                                                                          def List.findIdx {α : Type u_1} (p : αBool) (l : List α) :

                                                                          Returns the index of the first element satisfying p, or the length of the list otherwise.

                                                                          Equations
                                                                          Instances For
                                                                            @[specialize #[]]
                                                                            def List.findIdx.go {α : Type u_1} (p : αBool) :
                                                                            List αNatNat

                                                                            Auxiliary for findIdx: findIdx.go p l n = findIdx p l + n

                                                                            Equations
                                                                            Instances For
                                                                              def List.indexOf {α : Type u_1} [BEq α] (a : α) :
                                                                              List αNat

                                                                              Returns the index of the first element equal to a, or the length of the list otherwise.

                                                                              Equations
                                                                              Instances For
                                                                                def List.removeNth {α : Type u_1} :
                                                                                List αNatList α

                                                                                Removes the nth element of l, or the original list if n is out of bounds.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def List.removeNthTR {α : Type u_1} (l : List α) (n : Nat) :
                                                                                  List α

                                                                                  Tail recursive version of removeNth.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def List.removeNthTR.go {α : Type u_1} (l : List α) :
                                                                                    List αNatArray αList α

                                                                                    Auxiliary for removeNthTR: removeNthTR.go l xs n acc = acc.toList ++ removeNth xs n if n < length xs, else l.

                                                                                    Equations
                                                                                    Instances For
                                                                                      def List.replaceF {α : Type u_1} (f : αOption α) :
                                                                                      List αList α

                                                                                      Replaces the first element of the list for which f returns some with the returned value.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        def List.replaceFTR {α : Type u_1} (f : αOption α) (l : List α) :
                                                                                        List α

                                                                                        Tail-recursive version of replaceF.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[specialize #[]]
                                                                                          def List.replaceFTR.go {α : Type u_1} (f : αOption α) :
                                                                                          List αArray αList α

                                                                                          Auxiliary for replaceFTR: replaceFTR.go f xs acc = acc.toList ++ replaceF f xs.

                                                                                          Equations
                                                                                          Instances For
                                                                                            theorem List.replaceF_eq_replaceFTR.go (α : Type u_1) (p : αOption α) (acc : Array α) (xs : List α) :
                                                                                            List.replaceFTR.go p xs acc = acc.data ++ List.replaceF p xs
                                                                                            @[inline]
                                                                                            def List.insert {α : Type u_1} [DecidableEq α] (a : α) (l : List α) :
                                                                                            List α

                                                                                            Inserts an element into a list without duplication.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[inline]
                                                                                              def List.union {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
                                                                                              List α

                                                                                              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
                                                                                                instance List.instUnionList {α : Type u_1} [DecidableEq α] :
                                                                                                Union (List α)
                                                                                                Equations
                                                                                                • List.instUnionList = { union := List.union }
                                                                                                @[inline]
                                                                                                def List.inter {α : Type u_1} [DecidableEq α] (l₁ : List α) (l₂ : List α) :
                                                                                                List α

                                                                                                Constructs the intersection of two lists, by filtering the elements of l₁ that are in l₂. Unlike bagInter this does not preserve multiplicity: [1, 1].inter [1] is [1, 1].

                                                                                                Equations
                                                                                                Instances For
                                                                                                  instance List.instInterList {α : Type u_1} [DecidableEq α] :
                                                                                                  Inter (List α)
                                                                                                  Equations
                                                                                                  • List.instInterList = { inter := List.inter }
                                                                                                  inductive List.Sublist {α : Type u_1} :
                                                                                                  List αList αProp
                                                                                                  • 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 of l₂, then it is also a subsequence of a :: l₂.

                                                                                                  • cons₂: ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), List.Sublist l₁ l₂List.Sublist (a :: l₁) (a :: l₂)

                                                                                                    If l₁ is a subsequence of l₂, then a :: l₁ is a subsequence of a :: 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₂.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      def List.isSublist {α : Type u_1} [DecidableEq α] :
                                                                                                      List αList αBool

                                                                                                      True if the first list is a potentially non-contiguous sub-sequence of the second list.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def List.splitAt {α : Type u_1} (n : Nat) (l : List α) :
                                                                                                        List α × List α

                                                                                                        Split a list at an index.

                                                                                                        splitAt 2 [a, b, c] = ([a, b], [c])
                                                                                                        
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def List.splitAt.go {α : Type u_1} (l : List α) :
                                                                                                          List αNatArray αList α × List α

                                                                                                          Auxiliary for splitAt: splitAt.go l n xs acc = (acc.toList ++ take n xs, drop n xs) if n < length xs, else (l, []).

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def List.splitAtD {α : Type u_1} (n : Nat) (l : List α) (dflt : α) :
                                                                                                            List α × List α

                                                                                                            Split a list at an index. Ensures the left list always has the specified length by right padding with the provided default element.

                                                                                                            splitAtD 2 [a, b, c] x = ([a, b], [c])
                                                                                                            splitAtD 4 [a, b, c] x = ([a, b, c, x], [])
                                                                                                            
                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              def List.splitAtD.go {α : Type u_1} (dflt : α) :
                                                                                                              NatList αArray αList α × List α

                                                                                                              Auxiliary for splitAtD: splitAtD.go dflt n l acc = (acc.toList ++ left, right) if splitAtD n l dflt = (left, right).

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                def List.splitOnP {α : Type u_1} (P : αBool) (l : List α) :
                                                                                                                List (List α)

                                                                                                                Split a list at every element satisfying a predicate. The separators are not in the result.

                                                                                                                [1, 1, 2, 3, 2, 4, 4].splitOnP (· == 2) = [[1, 1], [3], [4, 4]]
                                                                                                                
                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  def List.splitOnP.go {α : Type u_1} (P : αBool) :
                                                                                                                  List αList αList (List α)

                                                                                                                  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
                                                                                                                  Instances For
                                                                                                                    @[inline]
                                                                                                                    def List.splitOnPTR {α : Type u_1} (P : αBool) (l : List α) :
                                                                                                                    List (List α)

                                                                                                                    Tail recursive version of removeNth.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[specialize #[]]
                                                                                                                      def List.splitOnPTR.go {α : Type u_1} (P : αBool) :
                                                                                                                      List αArray αArray (List α)List (List α)

                                                                                                                      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
                                                                                                                        @[inline]
                                                                                                                        def List.splitOn {α : Type u_1} [BEq α] (a : α) (as : List α) :
                                                                                                                        List (List α)

                                                                                                                        Split a list at every occurrence of a separator element. The separators are not in the result.

                                                                                                                        [1, 1, 2, 3, 2, 4, 4].splitOn 2 = [[1, 1], [3], [4, 4]]
                                                                                                                        
                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          def List.modifyNthTail {α : Type u_1} (f : List αList α) :
                                                                                                                          NatList αList α

                                                                                                                          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
                                                                                                                          Instances For
                                                                                                                            @[inline]
                                                                                                                            def List.modifyHead {α : Type u_1} (f : αα) :
                                                                                                                            List αList α

                                                                                                                            Apply f to the head of the list, if it exists.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              def List.modifyNth {α : Type u_1} (f : αα) :
                                                                                                                              NatList αList α

                                                                                                                              Apply f to the nth element of the list, if it exists.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                def List.modifyNthTR {α : Type u_1} (f : αα) (n : Nat) (l : List α) :
                                                                                                                                List α

                                                                                                                                Tail-recursive version of modifyNth.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  def List.modifyNthTR.go {α : Type u_1} (f : αα) :
                                                                                                                                  List αNatArray αList α

                                                                                                                                  Auxiliary for modifyNthTR: modifyNthTR.go f l n acc = acc.toList ++ modifyNth f n l.

                                                                                                                                  Equations
                                                                                                                                  Instances For
                                                                                                                                    theorem List.modifyNthTR_go_eq :
                                                                                                                                    ∀ {α : Type u_1} {f : αα} {acc : Array α} (l : List α) (n : Nat), List.modifyNthTR.go f l n acc = acc.data ++ List.modifyNth f n l
                                                                                                                                    @[inline]
                                                                                                                                    def List.modifyLast {α : Type u_1} (f : αα) (l : List α) :
                                                                                                                                    List α

                                                                                                                                    Apply f to the last element of l, if it exists.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      @[specialize #[]]
                                                                                                                                      def List.modifyLast.go {α : Type u_1} (f : αα) :
                                                                                                                                      List αArray αList α

                                                                                                                                      Auxiliary for modifyLast: modifyLast.go f l acc = acc.toList ++ modifyLast f l.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        def List.insertNth {α : Type u_1} (n : Nat) (a : α) :
                                                                                                                                        List αList α

                                                                                                                                        insertNth n a l inserts a into the list l after the first n elements of l

                                                                                                                                        insertNth 2 1 [1, 2, 3, 4] = [1, 2, 1, 3, 4]
                                                                                                                                        
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline]
                                                                                                                                          def List.insertNthTR {α : Type u_1} (n : Nat) (a : α) (l : List α) :
                                                                                                                                          List α

                                                                                                                                          Tail-recursive version of insertNth.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def List.insertNthTR.go {α : Type u_1} (a : α) :
                                                                                                                                            NatList αArray αList α

                                                                                                                                            Auxiliary for insertNthTR: insertNthTR.go a n l acc = acc.toList ++ insertNth n a l.

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              theorem List.insertNthTR_go_eq :
                                                                                                                                              ∀ {α : Type u_1} {a : α} {acc : Array α} (n : Nat) (l : List α), List.insertNthTR.go a n l acc = acc.data ++ List.insertNth n a l
                                                                                                                                              @[simp]
                                                                                                                                              theorem List.headD_eq_head? {α : Type u_1} (l : List α) (a : α) :
                                                                                                                                              def List.takeD {α : Type u_1} :
                                                                                                                                              NatList ααList α

                                                                                                                                              Take n elements from a list l. If l has less than n elements, append n - length l elements x.

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.takeD_zero {α : Type u_1} (l : List α) (a : α) :
                                                                                                                                                List.takeD 0 l a = []
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.takeD_succ {α : Type u_1} {n : Nat} (l : List α) (a : α) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem List.takeD_nil {α : Type u_1} (n : Nat) (a : α) :
                                                                                                                                                def List.takeDTR {α : Type u_1} (n : Nat) (l : List α) (dflt : α) :
                                                                                                                                                List α

                                                                                                                                                Tail-recursive version of takeD.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  def List.takeDTR.go {α : Type u_1} (dflt : α) :
                                                                                                                                                  NatList αArray αList α

                                                                                                                                                  Auxiliary for takeDTR: takeDTR.go dflt n l acc = acc.toList ++ takeD n l dflt.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    theorem List.takeDTR_go_eq :
                                                                                                                                                    ∀ {α : Type u_1} {dflt : α} {acc : Array α} (n : Nat) (l : List α), List.takeDTR.go dflt n l acc = acc.data ++ List.takeD n l dflt
                                                                                                                                                    def List.leftpad {α : Type u_1} (n : Nat) (a : α) (l : List α) :
                                                                                                                                                    List α

                                                                                                                                                    Pads l : List α with repeated occurrences of a : α until it is of length n. If l is initially larger than n, just return l.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      @[inline]
                                                                                                                                                      def List.leftpadTR {α : Type u_1} (n : Nat) (a : α) (l : List α) :
                                                                                                                                                      List α

                                                                                                                                                      Optimized version of leftpad.

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        def List.scanl {α : Type u_1} {β : Type u_2} (f : αβα) (a : α) :
                                                                                                                                                        List βList α

                                                                                                                                                        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
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def List.scanlTR {α : Type u_1} {β : Type u_2} (f : αβα) (a : α) (l : List β) :
                                                                                                                                                          List α

                                                                                                                                                          Tail-recursive version of scanl.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            @[specialize #[]]
                                                                                                                                                            def List.scanlTR.go {α : Type u_1} {β : Type u_2} (f : αβα) :
                                                                                                                                                            List βαArray αList α

                                                                                                                                                            Auxiliary for scanlTR: scanlTR.go f l a acc = acc.toList ++ scanl f a l.

                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              theorem List.scanlTR_go_eq :
                                                                                                                                                              ∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1α} {a : α} {acc : Array α} (l : List α_1), List.scanlTR.go f l a acc = acc.data ++ List.scanl f a l
                                                                                                                                                              def List.scanr {α : Type u_1} {β : Type u_2} (f : αββ) (b : β) (l : List α) :
                                                                                                                                                              List β

                                                                                                                                                              Fold a function f over the list from the right, returning the list of partial results.

                                                                                                                                                              scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
                                                                                                                                                              
                                                                                                                                                              Equations
                                                                                                                                                              • List.scanr f b l = match List.foldr (fun a x => match x with | (b', l') => (f a b', b' :: l')) (b, []) l with | (b', l') => b' :: l'
                                                                                                                                                              Instances For
                                                                                                                                                                @[inline]
                                                                                                                                                                def List.partitionMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ γ) (l : List α) :
                                                                                                                                                                List β × List γ

                                                                                                                                                                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 : NatNatNat ⊕ Nat) [inl 0, inr 1, inl 2] = ([0, 2], [1])
                                                                                                                                                                
                                                                                                                                                                Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  @[specialize #[]]
                                                                                                                                                                  def List.partitionMap.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ γ) :
                                                                                                                                                                  List αArray βArray γList β × List γ

                                                                                                                                                                  Auxiliary for partitionMap: partitionMap.go f l acc₁ acc₂ = (acc₁.toList ++ left, acc₂.toList ++ right) if partitionMap f l = (left, right).

                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    @[inline]
                                                                                                                                                                    def List.partitionM {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) (l : List α) :
                                                                                                                                                                    m (List α × List α)

                                                                                                                                                                    Monadic generalization of List.partition.

                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[specialize #[]]
                                                                                                                                                                      def List.partitionM.go {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) :
                                                                                                                                                                      List αArray αArray αm (List α × List α)

                                                                                                                                                                      Auxiliary for partitionM: partitionM.go p l acc₁ acc₂ returns (acc₁.toList ++ left, acc₂.toList ++ right) if partitionM p l returns (left, right).

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[specialize #[]]
                                                                                                                                                                        def List.foldlIdx {α : Sort u_1} {β : Type u_2} (f : Natαβα) (init : α) :
                                                                                                                                                                        List βoptParam Nat 0α

                                                                                                                                                                        Fold a list from left to right as with foldl, but the combining function also receives each element's index.

                                                                                                                                                                        Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[specialize #[]]
                                                                                                                                                                          def List.foldrIdx {α : Type u_1} {β : Sort u_2} (f : Natαββ) (init : β) (l : List α) (start : optParam Nat 0) :
                                                                                                                                                                          β

                                                                                                                                                                          Fold a list from right to left as with foldr, but the combining function also receives each element's index.

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[inline]
                                                                                                                                                                            def List.findIdxs {α : Type u_1} (p : αBool) (l : List α) :

                                                                                                                                                                            findIdxs p l is the list of indexes of elements of l that satisfy p.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              @[inline]
                                                                                                                                                                              def List.indexesValues {α : Type u_1} (p : αBool) (l : List α) :
                                                                                                                                                                              List (Nat × α)

                                                                                                                                                                              Returns the elements of l that satisfy p together with their indexes in l. The returned list is ordered by index.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For
                                                                                                                                                                                @[inline]
                                                                                                                                                                                def List.indexesOf {α : Type u_1} [BEq α] (a : α) :
                                                                                                                                                                                List αList Nat

                                                                                                                                                                                indexesOf a l is the list of all indexes of a in l. For example:

                                                                                                                                                                                indexesOf a [a, b, a, a] = [0, 2, 3]
                                                                                                                                                                                
                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  def List.findIdx? {α : Type u_1} (p : αBool) :
                                                                                                                                                                                  List αoptParam Nat 0Option Nat

                                                                                                                                                                                  Return the index of the first occurrence of an element satisfying p.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[inline]
                                                                                                                                                                                    def List.indexOf? {α : Type u_1} [BEq α] (a : α) :
                                                                                                                                                                                    List αOption Nat

                                                                                                                                                                                    Return the index of the first occurrence of a in the list.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def List.pmap {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (l : List α) :
                                                                                                                                                                                      ((a : α) → a lp a) → List β

                                                                                                                                                                                      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
                                                                                                                                                                                        @[implemented_by _private.Std.Data.List.Basic.0.List.attachImpl]
                                                                                                                                                                                        def List.attach {α : Type u_1} (l : List α) :
                                                                                                                                                                                        List { x // x l }

                                                                                                                                                                                        "Attach" the proof that the elements of l are in l to produce a new list with the same elements but in the type {x // x ∈ l}.

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[inline]
                                                                                                                                                                                          def List.lookmap {α : Type u_1} (f : αOption α) (l : List α) :
                                                                                                                                                                                          List α

                                                                                                                                                                                          lookmap is a combination of lookup and filterMap. lookmap f l will apply f : α → Option α to each element of the list, replacing a → b at the first value a in the list such that f a = some b.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            @[specialize #[]]
                                                                                                                                                                                            def List.lookmap.go {α : Type u_1} (f : αOption α) :
                                                                                                                                                                                            List αArray αList α

                                                                                                                                                                                            Auxiliary for lookmap: lookmap.go f l acc = acc.toList ++ lookmap f l.

                                                                                                                                                                                            Equations
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[inline]
                                                                                                                                                                                              def List.countP {α : Type u_1} (p : αBool) (l : List α) :

                                                                                                                                                                                              countP p l is the number of elements of l that satisfy p.

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[specialize #[]]
                                                                                                                                                                                                def List.countP.go {α : Type u_1} (p : αBool) :
                                                                                                                                                                                                List αNatNat

                                                                                                                                                                                                Auxiliary for countP: countP.go p l acc = countP p l + acc.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                  def List.count {α : Type u_1} [BEq α] (a : α) :
                                                                                                                                                                                                  List αNat

                                                                                                                                                                                                  count a l is the number of occurrences of a in l.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    def List.isPrefix {α : Type u_1} (l₁ : List α) (l₂ : List α) :

                                                                                                                                                                                                    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.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • (l₁ <+: l₂) = t, l₁ ++ t = l₂
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def List.isSuffix {α : Type u_1} (l₁ : List α) (l₂ : List α) :

                                                                                                                                                                                                      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.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      • (l₁ <:+ l₂) = t, t ++ l₁ = l₂
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        def List.isInfix {α : Type u_1} (l₁ : List α) (l₂ : List α) :

                                                                                                                                                                                                        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.

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        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.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          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.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            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.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                def List.inits {α : Type u_1} :
                                                                                                                                                                                                                List αList (List α)

                                                                                                                                                                                                                inits l is the list of initial segments of l.

                                                                                                                                                                                                                inits [1, 2, 3] = [[], [1], [1, 2], [1, 2, 3]]
                                                                                                                                                                                                                
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  def List.initsTR {α : Type u_1} (l : List α) :
                                                                                                                                                                                                                  List (List α)

                                                                                                                                                                                                                  Tail-recursive version of inits.

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    def List.tails {α : Type u_1} :
                                                                                                                                                                                                                    List αList (List α)

                                                                                                                                                                                                                    tails l is the list of terminal segments of l.

                                                                                                                                                                                                                    tails [1, 2, 3] = [[1, 2, 3], [2, 3], [3], []]
                                                                                                                                                                                                                    
                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      def List.tailsTR {α : Type u_1} (l : List α) :
                                                                                                                                                                                                                      List (List α)

                                                                                                                                                                                                                      Tail-recursive version of tails.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        def List.tailsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) :
                                                                                                                                                                                                                        List (List α)

                                                                                                                                                                                                                        Auxiliary for tailsTR: tailsTR.go l acc = acc.toList ++ tails l.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          def List.sublists' {α : Type u_1} (l : List α) :
                                                                                                                                                                                                                          List (List α)

                                                                                                                                                                                                                          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
                                                                                                                                                                                                                            def List.sublists {α : Type u_1} (l : List α) :
                                                                                                                                                                                                                            List (List α)

                                                                                                                                                                                                                            sublists l is the list of all (non-contiguous) sublists of l; cf. sublists' for a different ordering.

                                                                                                                                                                                                                            sublists [1, 2, 3] = [[], [1], [2], [1, 2], [3], [1, 3], [2, 3], [1, 2, 3]]
                                                                                                                                                                                                                            
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              inductive List.Forall₂ {α : Type u_1} {β : Type u_2} (R : αβProp) :
                                                                                                                                                                                                                              List αList βProp

                                                                                                                                                                                                                              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
                                                                                                                                                                                                                                def List.transpose {α : Type u_1} (l : List (List α)) :
                                                                                                                                                                                                                                List (List α)

                                                                                                                                                                                                                                Transpose of a list of lists, treated as a matrix.

                                                                                                                                                                                                                                transpose [[1, 2], [3, 4], [5, 6]] = [[1, 3, 5], [2, 4, 6]]
                                                                                                                                                                                                                                
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  def List.transpose.pop {α : Type u_1} (old : List α) :
                                                                                                                                                                                                                                  List αId (List α × List α)

                                                                                                                                                                                                                                  pop : List α → StateM (List α) (List α) transforms the input list old by taking the head of the current state and pushing it on the head of old. If the state list is empty, then old is left unchanged.

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    def List.transpose.go {α : Type u_1} (l : List α) (acc : Array (List α)) :
                                                                                                                                                                                                                                    Array (List α)

                                                                                                                                                                                                                                    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
                                                                                                                                                                                                                                      def List.sections {α : Type u_1} :
                                                                                                                                                                                                                                      List (List α)List (List α)

                                                                                                                                                                                                                                      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
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        def List.sectionsTR {α : Type u_1} (L : List (List α)) :
                                                                                                                                                                                                                                        List (List α)

                                                                                                                                                                                                                                        Optimized version of sections.

                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          def List.sectionsTR.go {α : Type u_1} (l : List α) (acc : Array (List α)) :
                                                                                                                                                                                                                                          Array (List α)

                                                                                                                                                                                                                                          go : List α → Array (List α) → Array (List α) inserts one list into the accumulated list of sections acc: go [a, b] #[l₁, l₂] = [a::l₁, b::l₁, a::l₂, b::l₂].

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            theorem List.sections_eq_nil_of_isEmpty {α : Type u_1} {L : List (List α)} :
                                                                                                                                                                                                                                            List.any L List.isEmpty = trueList.sections L = []
                                                                                                                                                                                                                                            def List.eraseP {α : Type u_1} (p : αBool) :
                                                                                                                                                                                                                                            List αList α

                                                                                                                                                                                                                                            eraseP p l removes the first element of l satisfying the predicate p.

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                              def List.erasePTR {α : Type u_1} (p : αBool) (l : List α) :
                                                                                                                                                                                                                                              List α

                                                                                                                                                                                                                                              Tail-recursive version of eraseP.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                @[specialize #[]]
                                                                                                                                                                                                                                                def List.erasePTR.go {α : Type u_1} (p : αBool) (l : List α) :
                                                                                                                                                                                                                                                List αArray αList α

                                                                                                                                                                                                                                                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
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  theorem List.eraseP_eq_erasePTR.go (α : Type u_1) (p : αBool) (l : List α) (acc : Array α) (xs : List α) :
                                                                                                                                                                                                                                                  l = acc.data ++ xsList.erasePTR.go p l xs acc = acc.data ++ List.eraseP p xs
                                                                                                                                                                                                                                                  def List.extractP {α : Type u_1} (p : αBool) (l : List α) :
                                                                                                                                                                                                                                                  Option α × List α

                                                                                                                                                                                                                                                  extractP p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    def List.extractP.go {α : Type u_1} (p : αBool) (l : List α) :
                                                                                                                                                                                                                                                    List αArray αOption α × List α

                                                                                                                                                                                                                                                    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
                                                                                                                                                                                                                                                      def List.revzip {α : Type u_1} (l : List α) :
                                                                                                                                                                                                                                                      List (α × α)

                                                                                                                                                                                                                                                      revzip l returns a list of pairs of the elements of l paired with the elements of l in reverse order.

                                                                                                                                                                                                                                                      revzip [1, 2, 3, 4, 5] = [(1, 5), (2, 4), (3, 3), (4, 2), (5, 1)]
                                                                                                                                                                                                                                                      
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        def List.product {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
                                                                                                                                                                                                                                                        List (α × β)

                                                                                                                                                                                                                                                        product l₁ l₂ is the list of pairs (a, b) where a ∈ l₁ and b ∈ l₂.

                                                                                                                                                                                                                                                        product [1, 2] [5, 6] = [(1, 5), (1, 6), (2, 5), (2, 6)]
                                                                                                                                                                                                                                                        
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          def List.productTR {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) :
                                                                                                                                                                                                                                                          List (α × β)

                                                                                                                                                                                                                                                          Optimized version of product.

                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            def List.sigma {α : Type u_1} {σ : αType u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
                                                                                                                                                                                                                                                            List ((a : α) × σ a)

                                                                                                                                                                                                                                                            sigma l₁ l₂ is the list of dependent pairs (a, b) where a ∈ l₁ and b ∈ l₂ a.

                                                                                                                                                                                                                                                            sigma [1, 2] (λ_, [(5 : Nat), 6]) = [(1, 5), (1, 6), (2, 5), (2, 6)]
                                                                                                                                                                                                                                                            
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              def List.sigmaTR {α : Type u_1} {σ : αType u_2} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
                                                                                                                                                                                                                                                              List ((a : α) × σ a)

                                                                                                                                                                                                                                                              Optimized version of sigma.

                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                def List.ofFn {α : Type u_1} {n : Nat} (f : Fin nα) :
                                                                                                                                                                                                                                                                List α

                                                                                                                                                                                                                                                                ofFn f with f : fin n → α returns the list whose ith element is f i

                                                                                                                                                                                                                                                                ofFn f = [f 0, f 1, ... , f(n - 1)]
                                                                                                                                                                                                                                                                
                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  def List.ofFnNthVal {α : Type u_1} {n : Nat} (f : Fin nα) (i : Nat) :

                                                                                                                                                                                                                                                                  ofFnNthVal f i returns some (f i) if i < n and none otherwise.

                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    def List.Disjoint {α : Type u_1} (l₁ : List α) (l₂ : List α) :

                                                                                                                                                                                                                                                                    disjoint l₁ l₂ means that l₁ and l₂ have no elements in common.

                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      def List.takeWhile₂ {α : Type u_1} {β : Type u_2} (R : αβBool) :
                                                                                                                                                                                                                                                                      List αList βList α × List β

                                                                                                                                                                                                                                                                      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
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                        def List.takeWhile₂TR {α : Type u_1} {β : Type u_2} (R : αβBool) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                        List α × List β

                                                                                                                                                                                                                                                                        Tail-recursive version of takeWhile₂.

                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[specialize #[]]
                                                                                                                                                                                                                                                                          def List.takeWhile₂TR.go {α : Type u_1} {β : Type u_2} (R : αβBool) :
                                                                                                                                                                                                                                                                          List αList βList αList βList α × List β

                                                                                                                                                                                                                                                                          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
                                                                                                                                                                                                                                                                            theorem List.takeWhile₂_eq_takeWhile₂TR.go (α : Type u_2) (β : Type u_1) (R : αβBool) (as : List α) (bs : List β) (acca : List α) (accb : List β) :
                                                                                                                                                                                                                                                                            List.takeWhile₂TR.go R as bs acca accb = (List.reverse acca ++ (List.takeWhile₂ R as bs).fst, List.reverse accb ++ (List.takeWhile₂ R as bs).snd)
                                                                                                                                                                                                                                                                            inductive List.Pairwise {α : Type u_1} (R : ααProp) :
                                                                                                                                                                                                                                                                            List αProp

                                                                                                                                                                                                                                                                            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
                                                                                                                                                                                                                                                                              @[simp]
                                                                                                                                                                                                                                                                              theorem List.pairwise_cons {α : Type u_1} {R : ααProp} {a : α} {l : List α} :
                                                                                                                                                                                                                                                                              List.Pairwise R (a :: l) ((a' : α) → a' lR a a') List.Pairwise R l
                                                                                                                                                                                                                                                                              instance List.instDecidablePairwise {α : Type u_1} {R : ααProp} [DecidableRel R] (l : List α) :
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              def List.pwFilter {α : Type u_1} (R : ααProp) [DecidableRel R] (l : List α) :
                                                                                                                                                                                                                                                                              List α

                                                                                                                                                                                                                                                                              pwFilter R l is a maximal sublist of l which is Pairwise R. pwFilter (·≠·) is the erase duplicates function (cf. eraseDup), and pwFilter (·<·) finds a maximal increasing subsequence in l. For example,

                                                                                                                                                                                                                                                                              pwFilter (·<·) [0, 1, 5, 2, 6, 3, 4] = [0, 1, 2, 3, 4]
                                                                                                                                                                                                                                                                              
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                inductive List.Chain {α : Type u_1} (R : ααProp) :
                                                                                                                                                                                                                                                                                αList αProp
                                                                                                                                                                                                                                                                                • 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 bList.Chain R b lList.Chain R a (b :: l)

                                                                                                                                                                                                                                                                                  If a relates to b and b::l is a chain, then a :: 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
                                                                                                                                                                                                                                                                                  def List.Chain' {α : Type u_1} (R : ααProp) :
                                                                                                                                                                                                                                                                                  List αProp

                                                                                                                                                                                                                                                                                  Chain' R l means that R holds between adjacent elements of l.

                                                                                                                                                                                                                                                                                  Chain' R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
                                                                                                                                                                                                                                                                                  
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                    def List.Nodup {α : Type u_1} :
                                                                                                                                                                                                                                                                                    List αProp

                                                                                                                                                                                                                                                                                    Nodup l means that l has no duplicates, that is, any element appears at most once in the List. It is defined as Pairwise (≠).

                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      instance List.nodupDecidable {α : Type u_1} [DecidableEq α] (l : List α) :
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • List.nodupDecidable = List.instDecidablePairwise
                                                                                                                                                                                                                                                                                      @[inline]
                                                                                                                                                                                                                                                                                      def List.eraseDup {α : Type u_1} [DecidableEq α] :
                                                                                                                                                                                                                                                                                      List αList α

                                                                                                                                                                                                                                                                                      eraseDup l removes duplicates from l (taking only the first occurrence). Defined as pwFilter (≠).

                                                                                                                                                                                                                                                                                      eraseDup [1, 0, 2, 2, 1] = [0, 2, 1] 
                                                                                                                                                                                                                                                                                      
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        def List.range' (start : Nat) (len : Nat) (step : optParam Nat 1) :

                                                                                                                                                                                                                                                                                        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
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                          def List.range'TR (s : Nat) (n : Nat) (step : optParam Nat 1) :

                                                                                                                                                                                                                                                                                          Optimized version of range'.

                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                            def List.range'TR.go (step : optParam Nat 1) :
                                                                                                                                                                                                                                                                                            NatNatList NatList Nat

                                                                                                                                                                                                                                                                                            Auxiliary for range'TR: range'TR.go n e = [e-n, ..., e-1] ++ acc.

                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              theorem List.range'_eq_range'TR.go (step : optParam Nat 1) (s : Nat) (n : Nat) (m : Nat) :
                                                                                                                                                                                                                                                                                              List.range'TR.go step n (s + step * n) (List.range' (s + step * n) m step) = List.range' s (n + m) step
                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                              def List.reduceOption {α : Type u_1} :
                                                                                                                                                                                                                                                                                              List (Option α)List α

                                                                                                                                                                                                                                                                                              Drop nones from a list, and replace each remaining some a with a.

                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                def List.ilast' {α : Type u_1} :
                                                                                                                                                                                                                                                                                                αList αα

                                                                                                                                                                                                                                                                                                ilast' x xs returns the last element of xs if xs is non-empty; it returns x otherwise.

                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  def List.last' {α : Type u_1} :
                                                                                                                                                                                                                                                                                                  List αOption α

                                                                                                                                                                                                                                                                                                  last' xs returns the last element of xs if xs is non-empty; it returns none otherwise.

                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                    def List.rotate {α : Type u_1} (l : List α) (n : Nat) :
                                                                                                                                                                                                                                                                                                    List α

                                                                                                                                                                                                                                                                                                    rotate l n rotates the elements of l to the left by n

                                                                                                                                                                                                                                                                                                    rotate [0, 1, 2, 3, 4, 5] 2 = [2, 3, 4, 5, 0, 1]
                                                                                                                                                                                                                                                                                                    
                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                      def List.rotate' {α : Type u_1} :
                                                                                                                                                                                                                                                                                                      List αNatList α

                                                                                                                                                                                                                                                                                                      rotate' is the same as rotate, but slower. Used for proofs about rotate

                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                        def List.mapDiagM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : ααm β) (l : List α) :
                                                                                                                                                                                                                                                                                                        m (List β)

                                                                                                                                                                                                                                                                                                        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
                                                                                                                                                                                                                                                                                                          def List.mapDiagM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : ααm β) :
                                                                                                                                                                                                                                                                                                          List αArray βm (List β)

                                                                                                                                                                                                                                                                                                          Auxiliary for mapDiagM: mapDiagM.go as f acc = (acc.toList ++ ·) <$> mapDiagM f as

                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                            def List.forDiagM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] (f : ααm PUnit) :
                                                                                                                                                                                                                                                                                                            List αm PUnit

                                                                                                                                                                                                                                                                                                            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
                                                                                                                                                                                                                                                                                                              def List.getRest {α : Type u_1} [DecidableEq α] :
                                                                                                                                                                                                                                                                                                              List αList αOption (List α)

                                                                                                                                                                                                                                                                                                              getRest l l₁ returns some l₂ if l = l₁ ++ l₂. If l₁ is not a prefix of l, returns none

                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                def List.dropSlice {α : Type u_1} :
                                                                                                                                                                                                                                                                                                                NatNatList αList α

                                                                                                                                                                                                                                                                                                                List.dropSlice n m xs removes a slice of length m at index n in list xs.

                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                  def List.dropSliceTR {α : Type u_1} (n : Nat) (m : Nat) (l : List α) :
                                                                                                                                                                                                                                                                                                                  List α

                                                                                                                                                                                                                                                                                                                  Optimized version of dropSlice.

                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                    def List.dropSliceTR.go {α : Type u_1} (l : List α) (m : Nat) :
                                                                                                                                                                                                                                                                                                                    List αNatArray αList α

                                                                                                                                                                                                                                                                                                                    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
                                                                                                                                                                                                                                                                                                                      theorem List.dropSlice_zero₂ {α : Type u_1} (n : Nat) (l : List α) :
                                                                                                                                                                                                                                                                                                                      theorem List.dropSlice_eq_dropSliceTR.go (α : Type u_1) (l : List α) (m : Nat) (acc : Array α) (xs : List α) (n : Nat) :
                                                                                                                                                                                                                                                                                                                      l = acc.data ++ xsList.dropSliceTR.go l m xs n acc = acc.data ++ List.dropSlice n (m + 1) xs
                                                                                                                                                                                                                                                                                                                      def List.zipWithLeft' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) :
                                                                                                                                                                                                                                                                                                                      List αList βList γ × List β

                                                                                                                                                                                                                                                                                                                      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
                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                        def List.zipWithLeft'TR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                                                                        List γ × List β

                                                                                                                                                                                                                                                                                                                        Tail-recursive version of zipWithLeft'.

                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                          def List.zipWithLeft'TR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) :
                                                                                                                                                                                                                                                                                                                          List αList βArray γList γ × List β

                                                                                                                                                                                                                                                                                                                          Auxiliary for zipWithLeft'TR: zipWithLeft'TR.go l acc = acc.toList ++ zipWithLeft' l.

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                            theorem List.zipWithLeft'_eq_zipWithLeft'TR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : αOption βγ) (acc : Array γ) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                                                                            List.zipWithLeft'TR.go f as bs acc = match List.zipWithLeft' f as bs with | (l, r) => (Array.toList acc ++ l, r)
                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                            def List.zipWithRight' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option αβγ) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                                                                            List γ × List α

                                                                                                                                                                                                                                                                                                                            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
                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                              def List.zipLeft' {α : Type u_1} {β : Type u_2} :
                                                                                                                                                                                                                                                                                                                              List αList βList (α × Option β) × List β

                                                                                                                                                                                                                                                                                                                              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
                                                                                                                                                                                                                                                                                                                                @[inline]
                                                                                                                                                                                                                                                                                                                                def List.zipRight' {α : Type u_1} {β : Type u_2} :
                                                                                                                                                                                                                                                                                                                                List αList βList (Option α × β) × List α

                                                                                                                                                                                                                                                                                                                                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
                                                                                                                                                                                                                                                                                                                                  def List.zipWithLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) :
                                                                                                                                                                                                                                                                                                                                  List αList βList γ

                                                                                                                                                                                                                                                                                                                                  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
                                                                                                                                                                                                                                                                                                                                    @[inline]
                                                                                                                                                                                                                                                                                                                                    def List.zipWithLeftTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                                                                                    List γ

                                                                                                                                                                                                                                                                                                                                    Tail-recursive version of zipWithLeft.

                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                      def List.zipWithLeftTR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) :
                                                                                                                                                                                                                                                                                                                                      List αList βArray γList γ

                                                                                                                                                                                                                                                                                                                                      Auxiliary for zipWithLeftTR: zipWithLeftTR.go l acc = acc.toList ++ zipWithLeft l.

                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                        theorem List.zipWithLeft_eq_zipWithLeftTR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : αOption βγ) (acc : Array γ) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                        def List.zipWithRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option αβγ) (as : List α) (bs : List β) :
                                                                                                                                                                                                                                                                                                                                        List γ

                                                                                                                                                                                                                                                                                                                                        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
                                                                                                                                                                                                                                                                                                                                          @[inline]
                                                                                                                                                                                                                                                                                                                                          def List.zipLeft {α : Type u_1} {β : Type u_2} :
                                                                                                                                                                                                                                                                                                                                          List αList βList (α × Option β)

                                                                                                                                                                                                                                                                                                                                          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
                                                                                                                                                                                                                                                                                                                                            @[inline]
                                                                                                                                                                                                                                                                                                                                            def List.zipRight {α : Type u_1} {β : Type u_2} :
                                                                                                                                                                                                                                                                                                                                            List αList βList (Option α × β)

                                                                                                                                                                                                                                                                                                                                            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
                                                                                                                                                                                                                                                                                                                                              @[inline]
                                                                                                                                                                                                                                                                                                                                              def List.allSome {α : Type u_1} (l : List (Option α)) :

                                                                                                                                                                                                                                                                                                                                              If all elements of xs are some xᵢ, allSome xs returns the xᵢ. Otherwise it returns none.

                                                                                                                                                                                                                                                                                                                                              allSome [some 1, some 2] = some [1, 2]
                                                                                                                                                                                                                                                                                                                                              allSome [some 1, none  ] = none
                                                                                                                                                                                                                                                                                                                                              
                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                def List.fillNones {α : Type u_1} :
                                                                                                                                                                                                                                                                                                                                                List (Option α)List αList α

                                                                                                                                                                                                                                                                                                                                                fillNones xs ys replaces the nones in xs with elements of ys. If there are not enough ys to replace all the nones, the remaining nones are dropped from xs.

                                                                                                                                                                                                                                                                                                                                                fillNones [none, some 1, none, none] [2, 3] = [2, 1, 3]
                                                                                                                                                                                                                                                                                                                                                
                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                  @[inline]
                                                                                                                                                                                                                                                                                                                                                  def List.fillNonesTR {α : Type u_1} (as : List (Option α)) (as' : List α) :
                                                                                                                                                                                                                                                                                                                                                  List α

                                                                                                                                                                                                                                                                                                                                                  Tail-recursive version of fillNones.

                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                    def List.fillNonesTR.go {α : Type u_1} :
                                                                                                                                                                                                                                                                                                                                                    List (Option α)List αArray αList α

                                                                                                                                                                                                                                                                                                                                                    Auxiliary for fillNonesTR: fillNonesTR.go as as' acc = acc.toList ++ fillNones as as'.

                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                      theorem List.fillNones_eq_fillNonesTR.go (α : Type u_1) (acc : Array α) (as : List (Option α)) (as' : List α) :
                                                                                                                                                                                                                                                                                                                                                      List.fillNonesTR.go as as' acc = acc.data ++ List.fillNones as as'
                                                                                                                                                                                                                                                                                                                                                      def List.takeList {α : Type u_1} :
                                                                                                                                                                                                                                                                                                                                                      List αList NatList (List α) × List α

                                                                                                                                                                                                                                                                                                                                                      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
                                                                                                                                                                                                                                                                                                                                                        @[inline]
                                                                                                                                                                                                                                                                                                                                                        def List.takeListTR {α : Type u_1} (xs : List α) (ns : List Nat) :
                                                                                                                                                                                                                                                                                                                                                        List (List α) × List α

                                                                                                                                                                                                                                                                                                                                                        Tail-recursive version of takeList.

                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                          def List.takeListTR.go {α : Type u_1} :
                                                                                                                                                                                                                                                                                                                                                          List NatList αArray (List α)List (List α) × List α

                                                                                                                                                                                                                                                                                                                                                          Auxiliary for takeListTR: takeListTR.go as as' acc = acc.toList ++ takeList as as'.

                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                            theorem List.takeList_eq_takeListTR.go (α : Type u_1) (acc : Array (List α)) (ns : List Nat) (xs : List α) :
                                                                                                                                                                                                                                                                                                                                                            List.takeListTR.go ns xs acc = match List.takeList xs ns with | (l, r) => (Array.toList acc ++ l, r)
                                                                                                                                                                                                                                                                                                                                                            def List.toChunksAux {α : Type u_1} (n : Nat) :
                                                                                                                                                                                                                                                                                                                                                            List αNatList α × List (List α)

                                                                                                                                                                                                                                                                                                                                                            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
                                                                                                                                                                                                                                                                                                                                                              def List.toChunks {α : Type u_1} :
                                                                                                                                                                                                                                                                                                                                                              NatList αList (List α)

                                                                                                                                                                                                                                                                                                                                                              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
                                                                                                                                                                                                                                                                                                                                                                def List.toChunks.go {α : Type u_1} (n : Nat) :
                                                                                                                                                                                                                                                                                                                                                                List αArray αArray (List α)List (List α)

                                                                                                                                                                                                                                                                                                                                                                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.

                                                                                                                                                                                                                                                                                                                                                                  def List.zipWith₃ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβγδ) :
                                                                                                                                                                                                                                                                                                                                                                  List αList βList γList δ

                                                                                                                                                                                                                                                                                                                                                                  Ternary version of List.zipWith.

                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                    def List.zipWith₄ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : αβγδε) :
                                                                                                                                                                                                                                                                                                                                                                    List αList βList γList δList ε

                                                                                                                                                                                                                                                                                                                                                                    Quaternary version of List.zipWith.

                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                      def List.zipWith₅ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : αβγδεζ) :
                                                                                                                                                                                                                                                                                                                                                                      List αList βList γList δList εList ζ

                                                                                                                                                                                                                                                                                                                                                                      Quinary version of List.zipWith.

                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                        def List.mapWithPrefixSuffixAux {α : Type u_1} {β : Type u_2} (f : List ααList αβ) :
                                                                                                                                                                                                                                                                                                                                                                        List αList αList β

                                                                                                                                                                                                                                                                                                                                                                        An auxiliary function for List.mapWithPrefixSuffix.

                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                          def List.mapWithPrefixSuffix {α : Type u_1} {β : Type u_2} (f : List ααList αβ) (l : List α) :
                                                                                                                                                                                                                                                                                                                                                                          List β

                                                                                                                                                                                                                                                                                                                                                                          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 NatNat → 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
                                                                                                                                                                                                                                                                                                                                                                            def List.mapWithComplement {α : Type u_1} {β : Type u_2} (f : αList αβ) :
                                                                                                                                                                                                                                                                                                                                                                            List αList β

                                                                                                                                                                                                                                                                                                                                                                            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