Documentation

Init.Data.List.Basic

Basic operations on List. #

We define

In Init.Data.List.Impl we give tail-recursive versions of these operations along with @[csimp] lemmas,

In Init.Data.List.Lemmas we develop the full API for these functions.

Recall that length, get, set, fold, and concat have already been defined in Init.Prelude.

The operations are organized as follow:

Further operations are defined in Init.Data.List.BasicAux (because they use Array in their implementations), namely:

Preliminaries from Init.Prelude #

length #

@[simp]
theorem List.length_nil {α : Type u} :
[].length = 0
@[simp]
theorem List.length_singleton {α : Type u} (a : α) :
[a].length = 1
@[simp]
theorem List.length_cons {α : Type u_1} (a : α) (as : List α) :
(a :: as).length = as.length + 1

set #

@[simp]
theorem List.length_set {α : Type u} (as : List α) (i : Nat) (a : α) :
(as.set i a).length = as.length

foldl #

@[simp]
theorem List.foldl_nil :
∀ {α : Type u_1} {β : Type u_2} {f : αβα} {b : α}, List.foldl f b [] = b
@[simp]
theorem List.foldl_cons {α : Type u} {β : Type v} {a : α} {f : βαβ} (l : List α) (b : β) :
List.foldl f b (a :: l) = List.foldl f (f b a) l

concat #

@[simp]
theorem List.length_concat {α : Type u} (as : List α) (a : α) :
(as.concat a).length = as.length + 1
theorem List.of_concat_eq_concat {α : Type u} {as : List α} {bs : List α} {a : α} {b : α} (h : as.concat a = bs.concat b) :
as = bs a = b

Equality #

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.instBEq {α : Type u} [BEq α] :
    BEq (List α)
    Equations
    • List.instBEq = { beq := List.beq }
    instance List.instLawfulBEq {α : Type u} [BEq α] [LawfulBEq α] :
    Equations
    • =
    @[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
    • [].isEqv [] x = true
    • (a :: as).isEqv (b :: bs) x = (x a b && as.isEqv bs x)
    • x✝¹.isEqv x✝ x = false
    Instances For
      @[simp]
      theorem List.isEqv_nil_nil {α : Type u} {eqv : ααBool} :
      [].isEqv [] eqv = true
      @[simp]
      theorem List.isEqv_nil_cons {α : Type u} {a : α} {as : List α} {eqv : ααBool} :
      [].isEqv (a :: as) eqv = false
      @[simp]
      theorem List.isEqv_cons_nil {α : Type u} {a : α} {as : List α} {eqv : ααBool} :
      (a :: as).isEqv [] eqv = false
      theorem List.isEqv_cons₂ :
      ∀ {α : Type u_1} {a : α} {as : List α} {b : α} {bs : List α} {eqv : ααBool}, (a :: as).isEqv (b :: bs) eqv = (eqv a b && as.isEqv bs eqv)

      Lexicographic ordering #

      inductive List.lt {α : Type u} [LT α] :
      List αList αProp

      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.

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

        [] is the smallest element in the order.

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

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

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

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

      Instances For
        instance List.instLT {α : Type u} [LT α] :
        LT (List α)
        Equations
        • List.instLT = { 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
        • One or more equations did not get rendered due to their size.
        • [].hasDecidableLt [] = isFalse
        • [].hasDecidableLt (head :: tail) = isTrue
        • (head :: tail).hasDecidableLt [] = isFalse
        @[reducible]
        def List.le {α : Type u} [LT α] (a : List α) (b : List α) :

        The lexicographic order on lists.

        Equations
        Instances For
          instance List.instLEOfLT {α : Type u} [LT α] :
          LE (List α)
          Equations
          • List.instLEOfLT = { le := List.le }
          instance List.instDecidableLeOfDecidableRelLt {α : Type u} [LT α] [DecidableRel fun (x x_1 : α) => x < x_1] (l₁ : List α) (l₂ : List α) :
          Decidable (l₁ l₂)
          Equations

          Alternative getters #

          get? #

          def List.get? {α : Type u} (as : List α) (i : Nat) :

          Returns the i-th element in the list (zero-based).

          If the index is out of bounds (i ≥ as.length), this function returns none. Also see get, getD and get!.

          Equations
          • (a :: tail).get? 0 = some a
          • (head :: as).get? n.succ = as.get? n
          • x✝.get? x = none
          Instances For
            @[simp]
            theorem List.get?_nil {α : Type u} {n : Nat} :
            [].get? n = none
            @[simp]
            theorem List.get?_cons_zero {α : Type u} {a : α} {l : List α} :
            (a :: l).get? 0 = some a
            @[simp]
            theorem List.get?_cons_succ {α : Type u} {a : α} {l : List α} {n : Nat} :
            (a :: l).get? (n + 1) = l.get? n
            theorem List.ext_get? {α : Type u} {l₁ : List α} {l₂ : List α} :
            (∀ (n : Nat), l₁.get? n = l₂.get? n)l₁ = l₂
            @[reducible, inline, deprecated]
            abbrev List.ext {α : Type u_1} {l₁ : List α} {l₂ : List α} :
            (∀ (n : Nat), l₁.get? n = l₂.get? n)l₁ = l₂

            Deprecated alias for ext_get?. The preferred extensionality theorem is now ext_getElem?.

            Equations
            Instances For

              getD #

              def List.getD {α : Type u} (as : List α) (i : Nat) (fallback : α) :
              α

              Returns the i-th element in the list (zero-based).

              If the index is out of bounds (i ≥ as.length), this function returns fallback. See also get? and get!.

              Equations
              • as.getD i fallback = (as.get? i).getD fallback
              Instances For
                @[simp]
                theorem List.getD_nil {n : Nat} :
                ∀ {α : Type u_1} {d : α}, [].getD n d = d
                @[simp]
                theorem List.getD_cons_zero :
                ∀ {α : Type u_1} {x : α} {xs : List α} {d : α}, (x :: xs).getD 0 d = x
                @[simp]
                theorem List.getD_cons_succ :
                ∀ {α : Type u_1} {x : α} {xs : List α} {n : Nat} {d : α}, (x :: xs).getD (n + 1) d = xs.getD n d

                getLast #

                def List.getLast {α : Type u} (as : List α) :
                as []α

                Returns the last element of a non-empty list.

                Equations
                • [].getLast h = absurd h
                • [a].getLast x_2 = a
                • (head :: b :: as).getLast x_2 = (b :: as).getLast
                Instances For

                  getLast? #

                  def List.getLast? {α : Type u} :
                  List αOption α

                  Returns the last element in the list.

                  If the list is empty, this function returns none. Also see getLastD and getLast!.

                  Equations
                  • x.getLast? = match x with | [] => none | a :: as => some ((a :: as).getLast )
                  Instances For
                    @[simp]
                    theorem List.getLast?_nil {α : Type u} :
                    [].getLast? = none

                    getLastD #

                    def List.getLastD {α : Type u} (as : List α) (fallback : α) :
                    α

                    Returns the last element in the list.

                    If the list is empty, this function returns fallback. Also see getLast? and getLast!.

                    Equations
                    • x✝.getLastD x = match x✝, x with | [], a₀ => a₀ | a :: as, x => (a :: as).getLast
                    Instances For
                      @[simp]
                      theorem List.getLastD_nil {α : Type u} (a : α) :
                      [].getLastD a = a
                      @[simp]
                      theorem List.getLastD_cons {α : Type u} (a : α) (b : α) (l : List α) :
                      (b :: l).getLastD a = l.getLastD b

                      Head and tail #

                      def List.head {α : Type u} (as : List α) :
                      as []α

                      Returns the first element of a non-empty list.

                      Equations
                      • x✝.head x = match x✝, x with | a :: tail, x => a
                      Instances For
                        @[simp]
                        theorem List.head_cons {α : Type u} {a : α} {l : List α} {h : a :: l []} :
                        (a :: l).head h = a
                        def List.head? {α : Type u} :
                        List αOption α

                        Returns the first element in the list.

                        If the list is empty, this function returns none. Also see headD and head!.

                        Equations
                        • x.head? = match x with | [] => none | a :: tail => some a
                        Instances For
                          @[simp]
                          theorem List.head?_nil {α : Type u} :
                          [].head? = none
                          @[simp]
                          theorem List.head?_cons {α : Type u} {a : α} {l : List α} :
                          (a :: l).head? = some a

                          headD #

                          def List.headD {α : Type u} (as : List α) (fallback : α) :
                          α

                          Returns the first element in the list.

                          If the list is empty, this function returns fallback. Also see head? and head!.

                          Equations
                          • x✝.headD x = match x✝, x with | [], fallback => fallback | a :: tail, x => a
                          Instances For
                            @[simp]
                            theorem List.headD_nil {α : Type u} {d : α} :
                            [].headD d = d
                            @[simp]
                            theorem List.headD_cons {α : Type u} {a : α} {l : List α} {d : α} :
                            (a :: l).headD d = a

                            tail? #

                            def List.tail? {α : Type u} :
                            List αOption (List α)

                            Drops the first element of the list.

                            If the list is empty, this function returns none. Also see tailD and tail!.

                            Equations
                            • x.tail? = match x with | [] => none | head :: as => some as
                            Instances For
                              @[simp]
                              theorem List.tail?_nil {α : Type u} :
                              [].tail? = none
                              @[simp]
                              theorem List.tail?_cons {α : Type u} {a : α} {l : List α} :
                              (a :: l).tail? = some l

                              tailD #

                              def List.tailD {α : Type u} (list : List α) (fallback : List α) :
                              List α

                              Drops the first element of the list.

                              If the list is empty, this function returns fallback. Also see head? and head!.

                              Equations
                              • list.tailD fallback = match list with | [] => fallback | head :: tl => tl
                              Instances For
                                @[simp]
                                theorem List.tailD_nil {α : Type u} {l' : List α} :
                                [].tailD l' = l'
                                @[simp]
                                theorem List.tailD_cons {α : Type u} {a : α} {l : List α} {l' : List α} :
                                (a :: l).tailD l' = l

                                Basic List operations. #

                                We define the basic functional programming operations on List: map, filter, filterMap, foldr, append, join, pure, bind, replicate, and reverse.

                                map #

                                @[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
                                  @[simp]
                                  theorem List.map_nil {α : Type u} {β : Type v} {f : αβ} :
                                  List.map f [] = []
                                  @[simp]
                                  theorem List.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (l : List α) :
                                  List.map f (a :: l) = f a :: List.map f l

                                  filter #

                                  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
                                    @[simp]
                                    theorem List.filter_nil {α : Type u} (p : αBool) :
                                    List.filter p [] = []

                                    filterMap #

                                    @[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
                                      @[simp]
                                      theorem List.filterMap_nil {α : Type u} {β : Type v} (f : αOption β) :
                                      theorem List.filterMap_cons {α : Type u} {β : Type v} (f : αOption β) (a : α) (l : List α) :
                                      List.filterMap f (a :: l) = match f a with | none => List.filterMap f l | some b => b :: List.filterMap f l

                                      foldr #

                                      @[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
                                        @[simp]
                                        theorem List.foldr_nil :
                                        ∀ {α : Type u_1} {α_1 : Type u_2} {f : αα_1α_1} {b : α_1}, List.foldr f b [] = b
                                        @[simp]
                                        theorem List.foldr_cons {α : Type u} {a : α} :
                                        ∀ {α_1 : Type u_1} {f : αα_1α_1} {b : α_1} (l : List α), List.foldr f b (a :: l) = f a (List.foldr f b l)

                                        reverse #

                                        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
                                        • [].reverseAux x = x
                                        • (a :: l).reverseAux x = l.reverseAux (a :: x)
                                        Instances For
                                          @[simp]
                                          theorem List.reverseAux_nil :
                                          ∀ {α : Type u_1} {r : List α}, [].reverseAux r = r
                                          @[simp]
                                          theorem List.reverseAux_cons :
                                          ∀ {α : Type u_1} {a : α} {l r : List α}, (a :: l).reverseAux r = l.reverseAux (a :: r)
                                          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
                                          • as.reverse = as.reverseAux []
                                          Instances For
                                            @[simp]
                                            theorem List.reverse_nil {α : Type u} :
                                            [].reverse = []
                                            theorem List.reverseAux_reverseAux {α : Type u} (as : List α) (bs : List α) (cs : List α) :
                                            (as.reverseAux bs).reverseAux cs = bs.reverseAux ((as.reverseAux []).reverseAux cs)

                                            append #

                                            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
                                            • [].append x = x
                                            • (a :: l).append x = a :: l.append x
                                            Instances For
                                              def List.appendTR {α : Type u} (as : List α) (bs : List α) :
                                              List α

                                              Tail-recursive version of List.append.

                                              Most of the tail-recursive implementations are in Init.Data.List.Impl, but appendTR must be set up immediately, because otherwise Append (List α) instance below will not use it.

                                              Equations
                                              • as.appendTR bs = as.reverse.reverseAux bs
                                              Instances For
                                                instance List.instAppend {α : Type u} :
                                                Equations
                                                • List.instAppend = { append := List.append }
                                                @[simp]
                                                theorem List.append_eq {α : Type u} (as : List α) (bs : List α) :
                                                as.append bs = as ++ bs
                                                @[simp]
                                                theorem List.nil_append {α : 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_nil {α : Type u} (as : List α) :
                                                as ++ [] = as
                                                instance List.instLawfulIdentityHAppendNil {α : Type u} :
                                                Std.LawfulIdentity (fun (x x_1 : List α) => x ++ x_1) []
                                                Equations
                                                • =
                                                @[simp]
                                                theorem List.length_append {α : Type u} (as : List α) (bs : List α) :
                                                (as ++ bs).length = as.length + bs.length
                                                @[simp]
                                                theorem List.append_assoc {α : Type u} (as : List α) (bs : List α) (cs : List α) :
                                                as ++ bs ++ cs = as ++ (bs ++ cs)
                                                instance List.instAssociativeHAppend {α : Type u} :
                                                Std.Associative fun (x x_1 : List α) => x ++ x_1
                                                Equations
                                                • =
                                                theorem List.append_cons {α : Type u} (as : List α) (b : α) (bs : List α) :
                                                as ++ b :: bs = as ++ [b] ++ bs
                                                @[simp]
                                                theorem List.concat_eq_append {α : Type u} (as : List α) (a : α) :
                                                as.concat a = as ++ [a]
                                                theorem List.reverseAux_eq_append {α : Type u} (as : List α) (bs : List α) :
                                                as.reverseAux bs = as.reverseAux [] ++ bs
                                                @[simp]
                                                theorem List.reverse_cons {α : Type u} (a : α) (as : List α) :
                                                (a :: as).reverse = as.reverse ++ [a]

                                                join #

                                                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
                                                • [].join = []
                                                • (a :: as).join = a ++ as.join
                                                Instances For
                                                  @[simp]
                                                  theorem List.join_nil {α : Type u} :
                                                  [].join = []
                                                  @[simp]
                                                  theorem List.join_cons :
                                                  ∀ {α : Type u_1} {l : List α} {ls : List (List α)}, (l :: ls).join = l ++ ls.join

                                                  pure #

                                                  @[inline]
                                                  def List.pure {α : Type u} (a : α) :
                                                  List α

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

                                                  Equations
                                                  Instances For

                                                    bind #

                                                    @[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
                                                      @[simp]
                                                      theorem List.bind_nil {α : Type u} {β : Type v} (f : αList β) :
                                                      [].bind f = []
                                                      @[simp]
                                                      theorem List.bind_cons {α : Type u} {β : Type v} (x : α) (xs : List α) (f : αList β) :
                                                      (x :: xs).bind f = f x ++ xs.bind f
                                                      @[reducible, inline, deprecated List.bind_nil]
                                                      abbrev List.nil_bind {α : Type u_1} {β : Type u_2} (f : αList β) :
                                                      [].bind f = []
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline, deprecated List.bind_cons]
                                                        abbrev List.cons_bind {α : Type u_1} {β : Type u_2} (x : α) (xs : List α) (f : αList β) :
                                                        (x :: xs).bind f = f x ++ xs.bind f
                                                        Equations
                                                        Instances For

                                                          replicate #

                                                          def List.replicate {α : Type u} (n : Nat) (a : α) :
                                                          List α

                                                          replicate n a is n copies of a:

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem List.replicate_zero :
                                                            ∀ {α : Type u_1} {a : α}, List.replicate 0 a = []
                                                            theorem List.replicate_succ {α : Type u} (a : α) (n : Nat) :
                                                            @[simp]
                                                            theorem List.length_replicate {α : Type u} (n : Nat) (a : α) :
                                                            (List.replicate n a).length = n

                                                            List membership #

                                                            EmptyCollection #

                                                            Equations
                                                            • List.instEmptyCollection = { emptyCollection := [] }
                                                            @[simp]
                                                            theorem List.empty_eq {α : Type u} :
                                                            = []

                                                            isEmpty #

                                                            def List.isEmpty {α : Type u} :
                                                            List αBool

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

                                                            Equations
                                                            • x.isEmpty = match x with | [] => true | head :: tail => false
                                                            Instances For
                                                              @[simp]
                                                              theorem List.isEmpty_nil {α : Type u} :
                                                              [].isEmpty = true
                                                              @[simp]
                                                              theorem List.isEmpty_cons {α : Type u} {x : α} {xs : List α} :
                                                              (x :: xs).isEmpty = false

                                                              elem #

                                                              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
                                                                @[simp]
                                                                theorem List.elem_nil {α : Type u} {a : α} [BEq α] :
                                                                theorem List.elem_cons {α : Type u} {b : α} {bs : List α} [BEq α] {a : α} :
                                                                List.elem a (b :: bs) = match a == b with | true => true | false => List.elem a bs
                                                                @[deprecated]
                                                                def List.notElem {α : Type u} [BEq α] (a : α) (as : List α) :

                                                                notElem a l is !(elem a l).

                                                                Equations
                                                                Instances For

                                                                  contains #

                                                                  @[reducible, inline]
                                                                  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
                                                                    @[simp]
                                                                    theorem List.contains_nil {α : Type u} {a : α} [BEq α] :
                                                                    [].contains a = false

                                                                    Mem #

                                                                    inductive List.Mem {α : Type u} (a : α) :
                                                                    List αProp

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

                                                                    Instances For
                                                                      instance List.instMembership {α : Type u} :
                                                                      Equations
                                                                      • List.instMembership = { mem := List.Mem }
                                                                      theorem List.mem_of_elem_eq_true {α : Type u} [BEq α] [LawfulBEq α] {a : α} {as : List α} :
                                                                      List.elem a as = truea as
                                                                      theorem List.elem_eq_true_of_mem {α : Type u} [BEq α] [LawfulBEq α] {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
                                                                      instance List.decidableBEx {α : Type u} (p : αProp) [DecidablePred p] (l : List α) :
                                                                      Decidable (∃ (x : α), x l p x)
                                                                      Equations
                                                                      instance List.decidableBAll {α : Type u} (p : αProp) [DecidablePred p] (l : List α) :
                                                                      Decidable (∀ (x : α), x lp x)
                                                                      Equations

                                                                      Sublists #

                                                                      take #

                                                                      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
                                                                        @[simp]
                                                                        theorem List.take_nil {α : Type u} {i : Nat} :
                                                                        List.take i [] = []
                                                                        @[simp]
                                                                        theorem List.take_zero {α : Type u} (l : List α) :
                                                                        List.take 0 l = []
                                                                        @[simp]
                                                                        theorem List.take_cons_succ :
                                                                        ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.take (i + 1) (a :: as) = a :: List.take i as

                                                                        drop #

                                                                        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 [] = []
                                                                          @[simp]
                                                                          theorem List.drop_zero {α : Type u} (l : List α) :
                                                                          List.drop 0 l = l
                                                                          @[simp]
                                                                          theorem List.drop_succ_cons :
                                                                          ∀ {α : Type u_1} {a : α} {l : List α} {n : Nat}, List.drop (n + 1) (a :: l) = List.drop n l
                                                                          theorem List.drop_eq_nil_of_le {α : Type u} {as : List α} {i : Nat} (h : as.length i) :
                                                                          List.drop i as = []

                                                                          takeWhile #

                                                                          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
                                                                            @[simp]
                                                                            theorem List.takeWhile_nil {α : Type u} {p : αBool} :

                                                                            dropWhile #

                                                                            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
                                                                              @[simp]
                                                                              theorem List.dropWhile_nil {α : Type u} {p : αBool} :

                                                                              partition #

                                                                              @[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

                                                                                  dropLast #

                                                                                  def List.dropLast {α : Type u_1} :
                                                                                  List αList α

                                                                                  Removes the last element of the list.

                                                                                  Equations
                                                                                  • [].dropLast = []
                                                                                  • [head].dropLast = []
                                                                                  • (a :: as).dropLast = a :: as.dropLast
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem List.dropLast_nil {α : Type u} :
                                                                                    [].dropLast = []
                                                                                    @[simp]
                                                                                    theorem List.dropLast_single :
                                                                                    ∀ {α : Type u_1} {x : α}, [x].dropLast = []
                                                                                    @[simp]
                                                                                    theorem List.dropLast_cons₂ :
                                                                                    ∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast
                                                                                    @[simp]
                                                                                    theorem List.length_dropLast_cons {α : Type u} (a : α) (as : List α) :
                                                                                    (a :: as).dropLast.length = as.length

                                                                                    isPrefixOf #

                                                                                    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
                                                                                    • [].isPrefixOf x = true
                                                                                    • x.isPrefixOf [] = false
                                                                                    • (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem List.isPrefixOf_nil_left {α : Type u} {l : List α} [BEq α] :
                                                                                      [].isPrefixOf l = true
                                                                                      @[simp]
                                                                                      theorem List.isPrefixOf_cons_nil {α : Type u} {a : α} {as : List α} [BEq α] :
                                                                                      (a :: as).isPrefixOf [] = false
                                                                                      theorem List.isPrefixOf_cons₂ {α : Type u} {as : List α} {b : α} {bs : List α} [BEq α] {a : α} :
                                                                                      (a :: as).isPrefixOf (b :: bs) = (a == b && as.isPrefixOf bs)

                                                                                      isPrefixOf? #

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

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

                                                                                      Equations
                                                                                      • [].isPrefixOf? x = some x
                                                                                      • x.isPrefixOf? [] = none
                                                                                      • (a :: as).isPrefixOf? (b :: bs) = if (a == b) = true then as.isPrefixOf? bs else none
                                                                                      Instances For

                                                                                        isSuffixOf #

                                                                                        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
                                                                                        • l₁.isSuffixOf l₂ = l₁.reverse.isPrefixOf l₂.reverse
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem List.isSuffixOf_nil_left {α : Type u} {l : List α} [BEq α] :
                                                                                          [].isSuffixOf l = true

                                                                                          isSuffixOf? #

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

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

                                                                                          Equations
                                                                                          • l₁.isSuffixOf? l₂ = Option.map List.reverse (l₁.reverse.isPrefixOf? l₂.reverse)
                                                                                          Instances For

                                                                                            rotateLeft #

                                                                                            def List.rotateLeft {α : Type u} (xs : List α) (n : optParam Nat 1) :
                                                                                            List α

                                                                                            O(n). Rotates the elements of xs to the left such that the element at xs[i] rotates to xs[(i - n) % l.length].

                                                                                            Equations
                                                                                            • xs.rotateLeft n = let len := xs.length; if len 1 then xs else let n := n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem List.rotateLeft_nil {α : Type u} {n : Nat} :
                                                                                              [].rotateLeft n = []

                                                                                              rotateRight #

                                                                                              def List.rotateRight {α : Type u} (xs : List α) (n : optParam Nat 1) :
                                                                                              List α

                                                                                              O(n). Rotates the elements of xs to the right such that the element at xs[i] rotates to xs[(i + n) % l.length].

                                                                                              Equations
                                                                                              • xs.rotateRight n = let len := xs.length; if len 1 then xs else let n := len - n % len; let b := List.take n xs; let e := List.drop n xs; e ++ b
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem List.rotateRight_nil {α : Type u} {n : Nat} :
                                                                                                [].rotateRight n = []

                                                                                                Manipulating elements #

                                                                                                replace #

                                                                                                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
                                                                                                • [].replace x✝ x = []
                                                                                                • (a :: as).replace x✝ x = match x✝ == a with | true => x :: as | false => a :: as.replace x✝ x
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem List.replace_nil {α : Type u} {a : α} {b : α} [BEq α] :
                                                                                                  [].replace a b = []
                                                                                                  theorem List.replace_cons {α : Type u} {as : List α} {b : α} {c : α} [BEq α] {a : α} :
                                                                                                  (a :: as).replace b c = match b == a with | true => c :: as | false => a :: as.replace b c

                                                                                                  insert #

                                                                                                  @[inline]
                                                                                                  def List.insert {α : Type u} [BEq α] (a : α) (l : List α) :
                                                                                                  List α

                                                                                                  Inserts an element into a list without duplication.

                                                                                                  Equations
                                                                                                  Instances For

                                                                                                    erase #

                                                                                                    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
                                                                                                    • [].erase x = []
                                                                                                    • (a :: as).erase x = match a == x with | true => as | false => a :: as.erase x
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem List.erase_nil {α : Type u} [BEq α] (a : α) :
                                                                                                      [].erase a = []
                                                                                                      theorem List.erase_cons {α : Type u} [BEq α] (a : α) (b : α) (l : List α) :
                                                                                                      (b :: l).erase a = if (b == a) = true then l else b :: l.erase a

                                                                                                      eraseIdx #

                                                                                                      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
                                                                                                      • [].eraseIdx x = []
                                                                                                      • (head :: as).eraseIdx 0 = as
                                                                                                      • (a :: as).eraseIdx n.succ = a :: as.eraseIdx n
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        theorem List.eraseIdx_nil {α : Type u} {i : Nat} :
                                                                                                        [].eraseIdx i = []
                                                                                                        @[simp]
                                                                                                        theorem List.eraseIdx_cons_zero :
                                                                                                        ∀ {α : Type u_1} {a : α} {as : List α}, (a :: as).eraseIdx 0 = as
                                                                                                        @[simp]
                                                                                                        theorem List.eraseIdx_cons_succ :
                                                                                                        ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, (a :: as).eraseIdx (i + 1) = a :: as.eraseIdx i

                                                                                                        find? #

                                                                                                        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
                                                                                                          @[simp]
                                                                                                          theorem List.find?_nil {α : Type u} {p : αBool} :
                                                                                                          List.find? p [] = none
                                                                                                          theorem List.find?_cons :
                                                                                                          ∀ {α : Type u_1} {a : α} {as : List α} {p : αBool}, List.find? p (a :: as) = match p a with | true => some a | false => List.find? p as

                                                                                                          findSome? #

                                                                                                          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
                                                                                                            @[simp]
                                                                                                            theorem List.findSome?_nil {α : Type u} :
                                                                                                            ∀ {α_1 : Type u_1} {f : αOption α_1}, List.findSome? f [] = none
                                                                                                            theorem List.findSome?_cons {α : Type u} {β : Type v} {a : α} {as : List α} {f : αOption β} :
                                                                                                            List.findSome? f (a :: as) = match f a with | some b => some b | none => List.findSome? f as

                                                                                                            lookup #

                                                                                                            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
                                                                                                              @[simp]
                                                                                                              theorem List.lookup_nil {α : Type u} {β : Type v} {a : α} [BEq α] :
                                                                                                              List.lookup a [] = none
                                                                                                              theorem List.lookup_cons {α : Type u} :
                                                                                                              ∀ {β : Type u_1} {b : β} {es : List (α × β)} {a : α} [inst : BEq α] {k : α}, List.lookup a ((k, b) :: es) = match a == k with | true => some b | false => List.lookup a es

                                                                                                              Logical operations #

                                                                                                              any #

                                                                                                              def List.any {α : Type u} :
                                                                                                              List α(αBool)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

                                                                                                              Short-circuits upon encountering the first true.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem List.any_nil :
                                                                                                                ∀ {α : Type u_1} {f : αBool}, [].any f = false
                                                                                                                @[simp]
                                                                                                                theorem List.any_cons :
                                                                                                                ∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, (a :: l).any f = (f a || l.any f)

                                                                                                                all #

                                                                                                                def List.all {α : Type u} :
                                                                                                                List α(αBool)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

                                                                                                                Short-circuits upon encountering the first false.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem List.all_nil :
                                                                                                                  ∀ {α : Type u_1} {f : αBool}, [].all f = true
                                                                                                                  @[simp]
                                                                                                                  theorem List.all_cons :
                                                                                                                  ∀ {α : Type u_1} {a : α} {l : List α} {f : αBool}, (a :: l).all f = (f a && l.all f)

                                                                                                                  or #

                                                                                                                  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
                                                                                                                  • bs.or = bs.any id
                                                                                                                  Instances For
                                                                                                                    @[simp]
                                                                                                                    theorem List.or_nil :
                                                                                                                    [].or = false
                                                                                                                    @[simp]
                                                                                                                    theorem List.or_cons {a : Bool} {l : List Bool} :
                                                                                                                    (a :: l).or = (a || l.or)

                                                                                                                    and #

                                                                                                                    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
                                                                                                                    • bs.and = bs.all id
                                                                                                                    Instances For
                                                                                                                      @[simp]
                                                                                                                      theorem List.and_nil :
                                                                                                                      [].and = true
                                                                                                                      @[simp]
                                                                                                                      theorem List.and_cons {a : Bool} {l : List Bool} :
                                                                                                                      (a :: l).and = (a && l.and)

                                                                                                                      Zippers #

                                                                                                                      zipWith #

                                                                                                                      @[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
                                                                                                                        @[simp]
                                                                                                                        theorem List.zipWith_nil_left {α : Type u} {β : Type v} {γ : Type w} {l : List β} {f : αβγ} :
                                                                                                                        List.zipWith f [] l = []
                                                                                                                        @[simp]
                                                                                                                        theorem List.zipWith_nil_right {α : Type u} {β : Type v} {γ : Type w} {l : List α} {f : αβγ} :
                                                                                                                        List.zipWith f l [] = []
                                                                                                                        @[simp]
                                                                                                                        theorem List.zipWith_cons_cons {α : Type u} {β : Type v} {γ : Type w} {a : α} {as : List α} {b : β} {bs : List β} {f : αβγ} :
                                                                                                                        List.zipWith f (a :: as) (b :: bs) = f a b :: List.zipWith f as bs

                                                                                                                        zip #

                                                                                                                        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
                                                                                                                          @[simp]
                                                                                                                          theorem List.zip_nil_left {α : Type u} {β : Type v} {l : List β} :
                                                                                                                          [].zip l = []
                                                                                                                          @[simp]
                                                                                                                          theorem List.zip_nil_right {α : Type u} {β : Type v} {l : List α} :
                                                                                                                          l.zip [] = []
                                                                                                                          @[simp]
                                                                                                                          theorem List.zip_cons_cons :
                                                                                                                          ∀ {α : Type u_1} {a : α} {as : List α} {α_1 : Type u_2} {b : α_1} {bs : List α_1}, (a :: as).zip (b :: bs) = (a, b) :: as.zip bs

                                                                                                                          zipWithAll #

                                                                                                                          def List.zipWithAll {α : Type u} {β : Type v} {γ : Type w} (f : Option αOption βγ) :
                                                                                                                          List αList βList γ

                                                                                                                          O(max |xs| |ys|). Version of List.zipWith that continues to the end of both lists, passing none to one argument once the shorter list has run out.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            @[simp]
                                                                                                                            theorem List.zipWithAll_nil_right :
                                                                                                                            ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option αOption α_1α_2} {as : List α}, List.zipWithAll f as [] = List.map (fun (a : α) => f (some a) none) as
                                                                                                                            @[simp]
                                                                                                                            theorem List.zipWithAll_nil_left :
                                                                                                                            ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option αOption α_1α_2} {bs : List α_1}, List.zipWithAll f [] bs = List.map (fun (b : α_1) => f none (some b)) bs
                                                                                                                            @[simp]
                                                                                                                            theorem List.zipWithAll_cons_cons :
                                                                                                                            ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option αOption α_1α_2} {a : α} {as : List α} {b : α_1} {bs : List α_1}, List.zipWithAll f (a :: as) (b :: bs) = f (some a) (some b) :: List.zipWithAll f as bs

                                                                                                                            unzip #

                                                                                                                            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
                                                                                                                            • [].unzip = ([], [])
                                                                                                                            • ((a, b) :: t).unzip = match t.unzip with | (al, bl) => (a :: al, b :: bl)
                                                                                                                            Instances For
                                                                                                                              @[simp]
                                                                                                                              theorem List.unzip_nil {α : Type u} {β : Type v} :
                                                                                                                              [].unzip = ([], [])
                                                                                                                              @[simp]
                                                                                                                              theorem List.unzip_cons {α : Type u} {β : Type v} {t : List (α × β)} {h : α × β} :
                                                                                                                              (h :: t).unzip = match t.unzip with | (al, bl) => (h.fst :: al, h.snd :: bl)

                                                                                                                              Ranges and enumeration #

                                                                                                                              range #

                                                                                                                              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
                                                                                                                                  @[simp]

                                                                                                                                  iota #

                                                                                                                                  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
                                                                                                                                    @[simp]
                                                                                                                                    theorem List.iota_zero :
                                                                                                                                    @[simp]
                                                                                                                                    theorem List.iota_succ {i : Nat} :
                                                                                                                                    List.iota (i + 1) = (i + 1) :: List.iota i

                                                                                                                                    enumFrom #

                                                                                                                                    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
                                                                                                                                      @[simp]
                                                                                                                                      theorem List.enumFrom_nil {α : Type u} {i : Nat} :
                                                                                                                                      @[simp]
                                                                                                                                      theorem List.enumFrom_cons :
                                                                                                                                      ∀ {α : Type u_1} {a : α} {as : List α} {i : Nat}, List.enumFrom i (a :: as) = (i, a) :: List.enumFrom (i + 1) as

                                                                                                                                      enum #

                                                                                                                                      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
                                                                                                                                        @[simp]
                                                                                                                                        theorem List.enum_nil {α : Type u} :
                                                                                                                                        [].enum = []

                                                                                                                                        Minima and maxima #

                                                                                                                                        minimum? #

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

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

                                                                                                                                        Equations
                                                                                                                                        Instances For

                                                                                                                                          maximum? #

                                                                                                                                          def List.maximum? {α : Type u} [Max α] :
                                                                                                                                          List αOption α

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

                                                                                                                                          Equations
                                                                                                                                          Instances For

                                                                                                                                            Other list operations #

                                                                                                                                            The functions are currently mostly used in meta code, and do not have sufficient API developed for verification work.

                                                                                                                                            intersperse #

                                                                                                                                            def List.intersperse {α : Type u} (sep : α) :
                                                                                                                                            List αList α

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

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[simp]
                                                                                                                                              theorem List.intersperse_nil {α : Type u} (sep : α) :
                                                                                                                                              @[simp]
                                                                                                                                              theorem List.intersperse_single {α : Type u} {x : α} (sep : α) :
                                                                                                                                              List.intersperse sep [x] = [x]
                                                                                                                                              @[simp]
                                                                                                                                              theorem List.intersperse_cons₂ {α : Type u} {x : α} {y : α} {zs : List α} (sep : α) :
                                                                                                                                              List.intersperse sep (x :: y :: zs) = x :: sep :: List.intersperse sep (y :: zs)

                                                                                                                                              intercalate #

                                                                                                                                              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

                                                                                                                                                eraseDups #

                                                                                                                                                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

                                                                                                                                                    eraseReps #

                                                                                                                                                    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

                                                                                                                                                        span #

                                                                                                                                                        @[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

                                                                                                                                                            groupBy #

                                                                                                                                                            @[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

                                                                                                                                                                removeAll #

                                                                                                                                                                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