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, foldl, 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 αList α

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

                            Equations
                            • x.tail = match x with | [] => [] | head :: as => as
                            Instances For
                              @[simp]
                              theorem List.tail_nil {α : Type u} :
                              [].tail = []
                              @[simp]
                              theorem List.tail_cons {α : Type u} {a : α} {as : List α} :
                              (a :: as).tail = as

                              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

                                                              Additional functions #

                                                              leftpad and rightpad #

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

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

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

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

                                                                Equations
                                                                Instances For

                                                                  reduceOption #

                                                                  @[inline]
                                                                  def List.reduceOption {α : Type u_1} :
                                                                  List (Option α)List α

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

                                                                  Equations
                                                                  Instances For

                                                                    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_succ_cons :
                                                                                ∀ {α : 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

                                                                                            Subset #

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

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

                                                                                            Equations
                                                                                            • l₁.Subset l₂ = ∀ ⦃a : α⦄, a l₁a l₂
                                                                                            Instances For
                                                                                              instance List.instHasSubset {α : Type u} :
                                                                                              Equations
                                                                                              • List.instHasSubset = { Subset := List.Subset }
                                                                                              Equations

                                                                                              Sublist and isSublist #

                                                                                              inductive List.Sublist {α : Type u_1} :
                                                                                              List αList αProp

                                                                                              l₁ <+ l₂, or Sublist l₁ l₂, says that l₁ is a (non-contiguous) subsequence of l₂.

                                                                                              • slnil: ∀ {α : Type u_1}, [].Sublist []

                                                                                                the base case: [] is a sublist of []

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

                                                                                                If l₁ is a subsequence of l₂, then it is also a subsequence of a :: l₂.

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

                                                                                                If l₁ is a subsequence of l₂, then a :: l₁ is a subsequence of a :: l₂.

                                                                                              Instances For

                                                                                                l₁ <+ l₂, or Sublist l₁ l₂, says that l₁ is a (non-contiguous) subsequence of l₂.

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

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

                                                                                                  Equations
                                                                                                  • [].isSublist x = true
                                                                                                  • x.isSublist [] = false
                                                                                                  • (hd₁ :: tl₁).isSublist (hd₂ :: tl₂) = if (hd₁ == hd₂) = true then tl₁.isSublist tl₂ else (hd₁ :: tl₁).isSublist tl₂
                                                                                                  Instances For

                                                                                                    IsPrefix / isPrefixOf / isPrefixOf? #

                                                                                                    def List.IsPrefix {α : Type u} (l₁ : List α) (l₂ : List α) :

                                                                                                    IsPrefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      IsPrefix l₁ l₂, or l₁ <+: l₂, means that l₁ is a prefix of l₂, that is, l₂ has the form l₁ ++ t for some t.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        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)
                                                                                                          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

                                                                                                            IsSuffix / isSuffixOf / 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
                                                                                                              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
                                                                                                                def List.IsSuffix {α : Type u} (l₁ : List α) (l₂ : List α) :

                                                                                                                IsSuffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  IsSuffix l₁ l₂, or l₁ <:+ l₂, means that l₁ is a suffix of l₂, that is, l₂ has the form t ++ l₁ for some t.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    IsInfix #

                                                                                                                    def List.IsInfix {α : Type u} (l₁ : List α) (l₂ : List α) :

                                                                                                                    IsInfix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

                                                                                                                    Equations
                                                                                                                    Instances For

                                                                                                                      IsInfix l₁ l₂, or l₁ <:+: l₂, means that l₁ is a contiguous substring of l₂, that is, l₂ has the form s ++ l₁ ++ t for some s, t.

                                                                                                                      Equations
                                                                                                                      Instances For

                                                                                                                        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 = []

                                                                                                                            Pairwise, Nodup #

                                                                                                                            inductive List.Pairwise {α : Type u} (R : ααProp) :
                                                                                                                            List αProp

                                                                                                                            Pairwise R l means that all the elements with earlier indexes are R-related to all the elements with later indexes.

                                                                                                                            Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
                                                                                                                            

                                                                                                                            For example if R = (·≠·) then it asserts l has no duplicates, and if R = (·<·) then it asserts that l is (strictly) sorted.

                                                                                                                            Instances For
                                                                                                                              @[simp]
                                                                                                                              theorem List.pairwise_cons {α : Type u} {R : ααProp} {a : α} {l : List α} :
                                                                                                                              List.Pairwise R (a :: l) (∀ (a' : α), a' lR a a') List.Pairwise R l
                                                                                                                              instance List.instDecidablePairwise {α : Type u} {R : ααProp} [DecidableRel R] (l : List α) :
                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              • [].instDecidablePairwise = isTrue
                                                                                                                              def List.Nodup {α : Type u} :
                                                                                                                              List αProp

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

                                                                                                                              Equations
                                                                                                                              Instances For
                                                                                                                                instance List.nodupDecidable {α : Type u} [DecidableEq α] (l : List α) :
                                                                                                                                Decidable l.Nodup
                                                                                                                                Equations
                                                                                                                                • List.nodupDecidable = List.instDecidablePairwise

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

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

                                                                                                                                      Equations
                                                                                                                                      Instances For

                                                                                                                                        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

                                                                                                                                          Finding elements

                                                                                                                                          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

                                                                                                                                              findIdx #

                                                                                                                                              @[inline]
                                                                                                                                              def List.findIdx {α : Type u} (p : αBool) (l : List α) :

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

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

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

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem List.findIdx_nil {α : Type u_1} (p : αBool) :

                                                                                                                                                  indexOf #

                                                                                                                                                  def List.indexOf {α : Type u} [BEq α] (a : α) :
                                                                                                                                                  List αNat

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

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    @[simp]
                                                                                                                                                    theorem List.indexOf_nil {α : Type u} {x : α} [BEq α] :

                                                                                                                                                    findIdx? #

                                                                                                                                                    def List.findIdx? {α : Type u} (p : αBool) :
                                                                                                                                                    List αoptParam Nat 0Option Nat

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

                                                                                                                                                    Equations
                                                                                                                                                    Instances For

                                                                                                                                                      indexOf? #

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

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

                                                                                                                                                      Equations
                                                                                                                                                      Instances For

                                                                                                                                                        countP #

                                                                                                                                                        @[inline]
                                                                                                                                                        def List.countP {α : Type u} (p : αBool) (l : List α) :

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

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

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

                                                                                                                                                          Equations
                                                                                                                                                          Instances For

                                                                                                                                                            count #

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

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

                                                                                                                                                            Equations
                                                                                                                                                            Instances For

                                                                                                                                                              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 #

                                                                                                                                                                                def Nat.sum (l : List Nat) :

                                                                                                                                                                                Sum of a list of natural numbers.

                                                                                                                                                                                Equations
                                                                                                                                                                                Instances For
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Nat.sum_nil :
                                                                                                                                                                                  Nat.sum [] = 0
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Nat.sum_cons (a : Nat) (l : List Nat) :
                                                                                                                                                                                  Nat.sum (a :: l) = a + Nat.sum l

                                                                                                                                                                                  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]

                                                                                                                                                                                      range' #

                                                                                                                                                                                      def List.range' (start : Nat) (len : Nat) (step : optParam Nat 1) :

                                                                                                                                                                                      range' start len step is the list of numbers [start, start+step, ..., start+(len-1)*step]. It is intended mainly for proving properties of range and iota.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For

                                                                                                                                                                                        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