Documentation

Init.Data.List.Basic

instance List.instGetElemListNatLtInstLTNatLength {α : Type u} :
GetElem (List α) Nat α fun as i => i < List.length as
Equations
  • List.instGetElemListNatLtInstLTNatLength = { getElem := fun as i h => List.get as { val := i, isLt := h } }
@[simp]
theorem List.cons_getElem_zero {α : Type u} (a : α) (as : List α) (h : 0 < List.length (a :: as)) :
(a :: as)[0] = a
@[simp]
theorem List.cons_getElem_succ {α : Type u} (a : α) (as : List α) (i : Nat) (h : i + 1 < List.length (a :: as)) :
(a :: as)[i + 1] = as[i]
theorem List.length_add_eq_lengthTRAux {α : Type u} (as : List α) (n : Nat) :
@[simp]
theorem List.length_nil {α : Type u} :
def List.reverseAux {α : Type u} :
List αList αList α

Auxiliary for List.reverse. List.reverseAux l r = l.reverse ++ r, but it is defined directly.

Equations
Instances For
    def List.reverse {α : Type u} (as : List α) :
    List α

    O(|as|). Reverse of a list:

    • [1, 2, 3, 4].reverse = [4, 3, 2, 1]

    Note that because of the "functional but in place" optimization implemented by Lean's compiler, this function works without any allocations provided that the input list is unshared: it simply walks the linked list and reverses all the node pointers.

    Equations
    Instances For
      theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) :
      @[simp]
      theorem List.reverse_reverse {α : Type u} (as : List α) :
      def List.append {α : Type u} (xs : List α) (ys : List α) :
      List α

      O(|xs|): append two lists. [1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]. It takes time proportional to the first list.

      Equations
      Instances For
        def List.appendTR {α : Type u} (as : List α) (bs : List α) :
        List α

        Tail-recursive version of List.append.

        Equations
        Instances For
          instance List.instAppendList {α : Type u} :
          Equations
          • List.instAppendList = { append := List.append }
          @[simp]
          theorem List.nil_append {α : Type u} (as : List α) :
          [] ++ as = as
          @[simp]
          theorem List.append_nil {α : Type u} (as : List α) :
          as ++ [] = as
          @[simp]
          theorem List.cons_append {α : Type u} (a : α) (as : List α) (bs : List α) :
          a :: as ++ bs = a :: (as ++ bs)
          @[simp]
          theorem List.append_eq {α : Type u} (as : List α) (bs : List α) :
          List.append as bs = as ++ bs
          theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) :
          as ++ bs ++ cs = as ++ (bs ++ cs)
          theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) :
          as ++ b :: bs = as ++ [b] ++ bs
          Equations
          • List.instEmptyCollectionList = { emptyCollection := [] }
          def List.erase {α : Type u_1} [BEq α] :
          List ααList α

          O(|l|). erase l a removes the first occurrence of a from l.

          • erase [1, 5, 3, 2, 5] 5 = [1, 3, 2, 5]
          • erase [1, 5, 3, 2, 5] 6 = [1, 5, 3, 2, 5]
          Equations
          Instances For
            def List.eraseIdx {α : Type u} :
            List αNatList α

            O(i). eraseIdx l i removes the i'th element of the list l.

            • erase [a, b, c, d, e] 0 = [b, c, d, e]
            • erase [a, b, c, d, e] 1 = [a, c, d, e]
            • erase [a, b, c, d, e] 5 = [a, b, c, d, e]
            Equations
            Instances For
              def List.isEmpty {α : Type u} :
              List αBool

              O(1). isEmpty l is true if the list is empty.

              Equations
              Instances For
                @[specialize #[]]
                def List.map {α : Type u} {β : Type v} (f : αβ) :
                List αList β

                O(|l|). map f l applies f to each element of the list.

                • map f [a, b, c] = [f a, f b, f c]
                Equations
                Instances For
                  @[inline]
                  def List.mapTR {α : Type u} {β : Type v} (f : αβ) (as : List α) :
                  List β

                  Tail-recursive version of List.map.

                  Equations
                  Instances For
                    @[specialize #[]]
                    def List.mapTR.loop {α : Type u} {β : Type v} (f : αβ) :
                    List αList βList β
                    Equations
                    Instances For
                      theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) :
                      @[simp]
                      theorem List.reverse_nil {α : Type u} :
                      @[simp]
                      theorem List.reverse_cons {α : Type u} (a : α) (as : List α) :
                      @[simp]
                      theorem List.reverse_append {α : Type u} (as : List α) (bs : List α) :
                      theorem List.mapTR_loop_eq {α : Type u} {β : Type v} (f : αβ) (as : List α) (bs : List β) :
                      def List.join {α : Type u} :
                      List (List α)List α

                      O(|join L|). join L concatenates all the lists in L into one list.

                      • join [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]
                      Equations
                      Instances For
                        @[specialize #[]]
                        def List.filterMap {α : Type u} {β : Type v} (f : αOption β) :
                        List αList β

                        O(|l|). filterMap f l takes a function f : α → Option β and applies it to each element of l; the resulting non-none values are collected to form the output list.

                        filterMap
                          (fun x => if x > 2 then some (2 * x) else none)
                          [1, 2, 5, 2, 7, 7]
                        = [10, 14, 14]
                        
                        Equations
                        Instances For
                          def List.filter {α : Type u} (p : αBool) :
                          List αList α

                          O(|l|). filter f l returns the list of elements in l for which f returns true.

                          filter (· > 2) [1, 2, 5, 2, 7, 7] = [5, 7, 7]
                          
                          Equations
                          Instances For
                            @[inline]
                            def List.filterTR {α : Type u} (p : αBool) (as : List α) :
                            List α

                            Tail-recursive version of List.filter.

                            Equations
                            Instances For
                              @[specialize #[]]
                              def List.filterTR.loop {α : Type u} (p : αBool) :
                              List αList αList α
                              Equations
                              Instances For
                                theorem List.filterTR_loop_eq {α : Type u} (p : αBool) (as : List α) (bs : List α) :
                                @[inline]
                                def List.partition {α : Type u} (p : αBool) (as : List α) :
                                List α × List α

                                O(|l|). partition p l calls p on each element of l, partitioning the list into two lists (l_true, l_false) where l_true has the elements where p was true and l_false has the elements where p is false. partition p l = (filter p l, filter (not ∘ p) l), but it is slightly more efficient since it only has to do one pass over the list.

                                partition (· > 2) [1, 2, 5, 2, 7, 7] = ([5, 7, 7], [1, 2, 2])
                                
                                Equations
                                Instances For
                                  @[specialize #[]]
                                  def List.partition.loop {α : Type u} (p : αBool) :
                                  List αList α × List αList α × List α
                                  Equations
                                  Instances For
                                    def List.dropWhile {α : Type u} (p : αBool) :
                                    List αList α

                                    O(|l|). dropWhile p l removes elements from the list until it finds the first element for which p returns false; this element and everything after it is returned.

                                    dropWhile (· < 4) [1, 3, 2, 4, 2, 7, 4] = [4, 2, 7, 4]
                                    
                                    Equations
                                    Instances For
                                      def List.find? {α : Type u} (p : αBool) :
                                      List αOption α

                                      O(|l|). find? p l returns the first element for which p returns true, or none if no such element is found.

                                      • find? (· < 5) [7, 6, 5, 8, 1, 2, 6] = some 1
                                      • find? (· < 1) [7, 6, 5, 8, 1, 2, 6] = none
                                      Equations
                                      Instances For
                                        def List.findSome? {α : Type u} {β : Type v} (f : αOption β) :
                                        List αOption β

                                        O(|l|). findSome? f l applies f to each element of l, and returns the first non-none result.

                                        • findSome? (fun x => if x < 5 then some (10 * x) else none) [7, 6, 5, 8, 1, 2, 6] = some 10
                                        Equations
                                        Instances For
                                          def List.replace {α : Type u} [BEq α] :
                                          List αααList α

                                          O(|l|). replace l a b replaces the first element in the list equal to a with b.

                                          • replace [1, 4, 2, 3, 3, 7] 3 6 = [1, 4, 2, 6, 3, 7]
                                          • replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]
                                          Equations
                                          Instances For
                                            def List.elem {α : Type u} [BEq α] (a : α) :
                                            List αBool

                                            O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

                                            • elem 3 [1, 4, 2, 3, 3, 7] = true
                                            • elem 5 [1, 4, 2, 3, 3, 7] = false
                                            Equations
                                            Instances For
                                              def List.notElem {α : Type u} [BEq α] (a : α) (as : List α) :

                                              notElem a l is !(elem a l).

                                              Equations
                                              Instances For
                                                @[inline, reducible]
                                                abbrev List.contains {α : Type u} [BEq α] (as : List α) (a : α) :

                                                O(|l|). elem a l or l.contains a is true if there is an element in l equal to a.

                                                • elem 3 [1, 4, 2, 3, 3, 7] = true
                                                • elem 5 [1, 4, 2, 3, 3, 7] = false
                                                Equations
                                                Instances For
                                                  inductive List.Mem {α : Type u} (a : α) :
                                                  List αProp
                                                  • head: ∀ {α : Type u} {a : α} (as : List α), List.Mem a (a :: as)

                                                    The head of a list is a member: a ∈ a :: as.

                                                  • tail: ∀ {α : Type u} {a : α} (b : α) {as : List α}, List.Mem a asList.Mem a (b :: as)

                                                    A member of the tail of a list is a member of the list: a ∈ l → a ∈ b :: l.

                                                  a ∈ l is a predicate which asserts that a is in the list l. Unlike elem, this uses = instead of == and is suited for mathematical reasoning.

                                                  • a ∈ [x, y, z] ↔ a = x ∨ a = y ∨ a = z
                                                  Instances For
                                                    instance List.instMembershipList {α : Type u} :
                                                    Equations
                                                    • List.instMembershipList = { mem := List.Mem }
                                                    theorem List.mem_of_elem_eq_true {α : Type u} [DecidableEq α] {a : α} {as : List α} :
                                                    List.elem a as = truea as
                                                    theorem List.elem_eq_true_of_mem {α : Type u} [DecidableEq α] {a : α} {as : List α} (h : a as) :
                                                    theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) :
                                                    a asa as ++ bs
                                                    theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) :
                                                    b bsb as ++ bs
                                                    def List.eraseDups {α : Type u_1} [BEq α] (as : List α) :
                                                    List α

                                                    O(|l|^2). Erase duplicated elements in the list. Keeps the first occurrence of duplicated elements.

                                                    • eraseDups [1, 3, 2, 2, 3, 5] = [1, 3, 2, 5]
                                                    Equations
                                                    Instances For
                                                      def List.eraseDups.loop {α : Type u_1} [BEq α] :
                                                      List αList αList α
                                                      Equations
                                                      Instances For
                                                        def List.eraseReps {α : Type u_1} [BEq α] :
                                                        List αList α

                                                        O(|l|). Erase repeated adjacent elements. Keeps the first occurrence of each run.

                                                        • eraseReps [1, 3, 2, 2, 2, 3, 5] = [1, 3, 2, 3, 5]
                                                        Equations
                                                        Instances For
                                                          def List.eraseReps.loop {α : Type u_1} [BEq α] :
                                                          αList αList αList α
                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def List.span {α : Type u} (p : αBool) (as : List α) :
                                                            List α × List α

                                                            O(|l|). span p l splits the list l into two parts, where the first part contains the longest initial segment for which p returns true and the second part is everything else.

                                                            • span (· > 5) [6, 8, 9, 5, 2, 9] = ([6, 8, 9], [5, 2, 9])
                                                            • span (· > 10) [6, 8, 9, 5, 2, 9] = ([6, 8, 9, 5, 2, 9], [])
                                                            Equations
                                                            Instances For
                                                              @[specialize #[]]
                                                              def List.span.loop {α : Type u} (p : αBool) :
                                                              List αList αList α × List α
                                                              Equations
                                                              Instances For
                                                                @[specialize #[]]
                                                                def List.groupBy {α : Type u} (R : ααBool) :
                                                                List αList (List α)

                                                                O(|l|). groupBy R l splits l into chains of elements such that adjacent elements are related by R.

                                                                • groupBy (·==·) [1, 1, 2, 2, 2, 3, 2] = [[1, 1], [2, 2, 2], [3], [2]]
                                                                • groupBy (·<·) [1, 2, 5, 4, 5, 1, 4] = [[1, 2, 5], [4, 5], [1, 4]]
                                                                Equations
                                                                Instances For
                                                                  @[specialize #[]]
                                                                  def List.groupBy.loop {α : Type u} (R : ααBool) :
                                                                  List ααList αList (List α)List (List α)
                                                                  Equations
                                                                  Instances For
                                                                    def List.lookup {α : Type u} {β : Type v} [BEq α] :
                                                                    αList (α × β)Option β

                                                                    O(|l|). lookup a l treats l : List (α × β) like an association list, and returns the first β value corresponding to an α value in the list equal to a.

                                                                    • lookup 3 [(1, 2), (3, 4), (3, 5)] = some 4
                                                                    • lookup 2 [(1, 2), (3, 4), (3, 5)] = none
                                                                    Equations
                                                                    Instances For
                                                                      def List.removeAll {α : Type u} [BEq α] (xs : List α) (ys : List α) :
                                                                      List α

                                                                      O(|xs|). Computes the "set difference" of lists, by filtering out all elements of xs which are also in ys.

                                                                      • removeAll [1, 1, 5, 1, 2, 4, 5] [1, 2, 2] = [5, 4, 5]
                                                                      Equations
                                                                      Instances For
                                                                        def List.drop {α : Type u} :
                                                                        NatList αList α

                                                                        O(min n |xs|). Removes the first n elements of xs.

                                                                        • drop 0 [a, b, c, d, e] = [a, b, c, d, e]
                                                                        • drop 3 [a, b, c, d, e] = [d, e]
                                                                        • drop 6 [a, b, c, d, e] = []
                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem List.drop_nil {α : Type u} {i : Nat} :
                                                                          List.drop i [] = []
                                                                          theorem List.get_drop_eq_drop {α : Type u} (as : List α) (i : Nat) (h : i < List.length as) :
                                                                          as[i] :: List.drop (i + 1) as = List.drop i as
                                                                          def List.take {α : Type u} :
                                                                          NatList αList α

                                                                          O(min n |xs|). Returns the first n elements of xs, or the whole list if n is too large.

                                                                          • take 0 [a, b, c, d, e] = []
                                                                          • take 3 [a, b, c, d, e] = [a, b, c]
                                                                          • take 6 [a, b, c, d, e] = [a, b, c, d, e]
                                                                          Equations
                                                                          Instances For
                                                                            def List.takeWhile {α : Type u} (p : αBool) (xs : List α) :
                                                                            List α

                                                                            O(|xs|). Returns the longest initial segment of xs for which p returns true.

                                                                            Equations
                                                                            Instances For
                                                                              @[specialize #[]]
                                                                              def List.foldr {α : Type u} {β : Type v} (f : αββ) (init : β) :
                                                                              List αβ

                                                                              O(|l|). Applies function f to all of the elements of the list, from right to left.

                                                                              • foldr f init [a, b, c] = f a <| f b <| f c <| init
                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                def List.any {α : Type u} (l : List α) (p : αBool) :

                                                                                O(|l|). Returns true if p is true for any element of l.

                                                                                • any p [a, b, c] = p a || p b || p c
                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def List.all {α : Type u} (l : List α) (p : αBool) :

                                                                                  O(|l|). Returns true if p is true for every element of l.

                                                                                  • all p [a, b, c] = p a && p b && p c
                                                                                  Equations
                                                                                  Instances For
                                                                                    def List.or (bs : List Bool) :

                                                                                    O(|l|). Returns true if true is an element of the list of booleans l.

                                                                                    • or [a, b, c] = a || b || c
                                                                                    Equations
                                                                                    Instances For
                                                                                      def List.and (bs : List Bool) :

                                                                                      O(|l|). Returns true if every element of l is the value true.

                                                                                      • and [a, b, c] = a && b && c
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[specialize #[]]
                                                                                        def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (xs : List α) (ys : List β) :
                                                                                        List γ

                                                                                        O(min |xs| |ys|). Applies f to the two lists in parallel, stopping at the shorter list.

                                                                                        • zipWith f [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]
                                                                                        Equations
                                                                                        Instances For
                                                                                          def List.zip {α : Type u} {β : Type v} :
                                                                                          List αList βList (α × β)

                                                                                          O(min |xs| |ys|). Combines the two lists into a list of pairs, with one element from each list. The longer list is truncated to match the shorter list.

                                                                                          • zip [x₁, x₂, x₃] [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]
                                                                                          Equations
                                                                                          Instances For
                                                                                            def List.unzip {α : Type u} {β : Type v} :
                                                                                            List (α × β)List α × List β

                                                                                            O(|l|). Separates a list of pairs into two lists containing the first components and second components.

                                                                                            • unzip [(x₁, y₁), (x₂, y₂), (x₃, y₃)] = ([x₁, x₂, x₃], [y₁, y₂, y₃])
                                                                                            Equations
                                                                                            Instances For
                                                                                              def List.range (n : Nat) :

                                                                                              O(n). range n is the numbers from 0 to n exclusive, in increasing order.

                                                                                              • range 5 = [0, 1, 2, 3, 4]
                                                                                              Equations
                                                                                              Instances For
                                                                                                Equations
                                                                                                Instances For

                                                                                                  O(n). iota n is the numbers from 1 to n inclusive, in decreasing order.

                                                                                                  • iota 5 = [5, 4, 3, 2, 1]
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def List.iotaTR (n : Nat) :

                                                                                                    Tail-recursive version of iota.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      def List.enumFrom {α : Type u} :
                                                                                                      NatList αList (Nat × α)

                                                                                                      O(|l|). enumFrom n l is like enum but it allows you to specify the initial index.

                                                                                                      • enumFrom 5 [a, b, c] = [(5, a), (6, b), (7, c)]
                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def List.enum {α : Type u} :
                                                                                                        List αList (Nat × α)

                                                                                                        O(|l|). enum l pairs up each element with its index in the list.

                                                                                                        • enum [a, b, c] = [(0, a), (1, b), (2, c)]
                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          def List.intersperse {α : Type u} (sep : α) :
                                                                                                          List αList α

                                                                                                          O(|l|). intersperse sep l alternates sep and the elements of l:

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) :
                                                                                                            List α

                                                                                                            O(|xs|). intercalate sep xs alternates sep and the elements of xs:

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def List.bind {α : Type u} {β : Type v} (a : List α) (b : αList β) :
                                                                                                              List β

                                                                                                              bind xs f is the bind operation of the list monad. It applies f to each element of xs to get a list of lists, and then concatenates them all together.

                                                                                                              • [2, 3, 2].bind range = [0, 1, 0, 1, 2, 0, 1]
                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline]
                                                                                                                def List.pure {α : Type u} (a : α) :
                                                                                                                List α

                                                                                                                pure x = [x] is the pure operation of the list monad.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  inductive List.lt {α : Type u} [LT α] :
                                                                                                                  List αList αProp
                                                                                                                  • nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), List.lt [] (b :: bs)

                                                                                                                    [] is the smallest element in the order.

                                                                                                                  • head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < bList.lt (a :: as) (b :: bs)

                                                                                                                    If a < b then a::as < b::bs.

                                                                                                                  • tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α}, ¬a < b¬b < aList.lt as bsList.lt (a :: as) (b :: bs)

                                                                                                                    If a and b are equivalent and as < bs, then a::as < b::bs.

                                                                                                                  The lexicographic order on lists. [] < a::as, and a::as < b::bs if a < b or if a and b are equivalent and as < bs.

                                                                                                                  Instances For
                                                                                                                    instance List.instLTList {α : Type u} [LT α] :
                                                                                                                    LT (List α)
                                                                                                                    Equations
                                                                                                                    • List.instLTList = { lt := List.lt }
                                                                                                                    instance List.hasDecidableLt {α : Type u} [LT α] [h : DecidableRel fun x x_1 => x < x_1] (l₁ : List α) (l₂ : List α) :
                                                                                                                    Decidable (l₁ < l₂)
                                                                                                                    Equations
                                                                                                                    @[reducible]
                                                                                                                    def List.le {α : Type u} [LT α] (a : List α) (b : List α) :

                                                                                                                    The lexicographic order on lists.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      instance List.instLEList {α : Type u} [LT α] :
                                                                                                                      LE (List α)
                                                                                                                      Equations
                                                                                                                      • List.instLEList = { le := List.le }
                                                                                                                      instance List.instForAllListDecidableLeInstLEList {α : Type u} [LT α] [DecidableRel fun x x_1 => x < x_1] (l₁ : List α) (l₂ : List α) :
                                                                                                                      Decidable (l₁ l₂)
                                                                                                                      Equations
                                                                                                                      def List.isPrefixOf {α : Type u} [BEq α] :
                                                                                                                      List αList αBool

                                                                                                                      isPrefixOf l₁ l₂ returns true Iff l₁ is a prefix of l₂. That is, there exists a t such that l₂ == l₁ ++ t.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        def List.isPrefixOf? {α : Type u} [BEq α] :
                                                                                                                        List αList αOption (List α)

                                                                                                                        isPrefixOf? l₁ l₂ returns some t when l₂ == l₁ ++ t.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          def List.isSuffixOf {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) :

                                                                                                                          isSuffixOf l₁ l₂ returns true Iff l₁ is a suffix of l₂. That is, there exists a t such that l₂ == t ++ l₁.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def List.isSuffixOf? {α : Type u} [BEq α] (l₁ : List α) (l₂ : List α) :

                                                                                                                            isSuffixOf? l₁ l₂ returns some t when l₂ == t ++ l₁.

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              @[specialize #[]]
                                                                                                                              def List.isEqv {α : Type u} (as : List α) (bs : List α) (eqv : ααBool) :

                                                                                                                              O(min |as| |bs|). Returns true if as and bs have the same length, and they are pairwise related by eqv.

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                def List.beq {α : Type u} [BEq α] :
                                                                                                                                List αList αBool

                                                                                                                                The equality relation on lists asserts that they have the same length and they are pairwise BEq.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  instance List.instBEqList {α : Type u} [BEq α] :
                                                                                                                                  BEq (List α)
                                                                                                                                  Equations
                                                                                                                                  • List.instBEqList = { beq := List.beq }
                                                                                                                                  def List.replicate {α : Type u} (n : Nat) (a : α) :
                                                                                                                                  List α

                                                                                                                                  replicate n a is n copies of a:

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

                                                                                                                                    Tail-recursive version of List.replicate.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      def List.replicateTR.loop {α : Type u} (a : α) :
                                                                                                                                      NatList αList α
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        def List.dropLast {α : Type u_1} :
                                                                                                                                        List αList α

                                                                                                                                        Removes the last element of the list.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_replicate {α : Type u} (n : Nat) (a : α) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_concat {α : Type u} (as : List α) (a : α) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_dropLast_cons {α : Type u} (a : α) (as : List α) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_append {α : Type u} (as : List α) (bs : List α) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_map {α : Type u} {β : Type v} (as : List α) (f : αβ) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem List.length_reverse {α : Type u} (as : List α) :
                                                                                                                                          def List.maximum? {α : Type u} [Max α] :
                                                                                                                                          List αOption α

                                                                                                                                          Returns the largest element of the list, if it is not empty.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            def List.minimum? {α : Type u} [Min α] :
                                                                                                                                            List αOption α

                                                                                                                                            Returns the smallest element of the list, if it is not empty.

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : List.concat as a = List.concat bs b) :
                                                                                                                                              as = bs a = b
                                                                                                                                              theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) :
                                                                                                                                              List.concat as a = as ++ [a]
                                                                                                                                              theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : List.length as i) :
                                                                                                                                              List.drop i as = []