Documentation

Init.Data.List.BasicAux

The following functions can't be defined at Init.Data.List.Basic, because they depend on Init.Util, and Init.Util depends on Init.Data.List.Basic.

Alternative getters #

get! #

def List.get! {α : Type u_1} [Inhabited α] (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 panics when executed, and returns default. See get? and getD for safer alternatives.

Equations
  • (a :: tail).get! 0 = a
  • (head :: as).get! n.succ = as.get! n
  • x✝.get! x = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.get!" 28 18 "invalid index"
Instances For
    theorem List.get!_nil {α : Type u_1} [Inhabited α] (n : Nat) :
    [].get! n = default
    theorem List.get!_cons_succ {α : Type u_1} [Inhabited α] (l : List α) (a : α) (n : Nat) :
    (a :: l).get! (n + 1) = l.get! n
    theorem List.get!_cons_zero {α : Type u_1} [Inhabited α] (l : List α) (a : α) :
    (a :: l).get! 0 = a

    getLast! #

    def List.getLast! {α : Type u_1} [Inhabited α] :
    List αα

    Returns the last element in the list.

    If the list is empty, this function panics when executed, and returns default. See getLast and getLastD for safer alternatives.

    Equations
    • x.getLast! = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.getLast!" 44 13 "empty list" | a :: as => (a :: as).getLast
    Instances For

      Head and tail #

      def List.head! {α : Type u_1} [Inhabited α] :
      List αα

      Returns the first element in the list.

      If the list is empty, this function panics when executed, and returns default. See head and headD for safer alternatives.

      Equations
      • x.head! = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.head!" 58 12 "empty list" | a :: tail => a
      Instances For

        tail! #

        def List.tail! {α : Type u_1} :
        List αList α

        Drops the first element of the list.

        If the list is empty, this function panics when executed, and returns the empty list. See tail and tailD for safer alternatives.

        Equations
        • x.tail! = match x with | [] => panicWithPosWithDecl "Init.Data.List.BasicAux" "List.tail!" 70 13 "empty list" | head :: as => as
        Instances For
          @[simp]
          theorem List.tail!_cons {α : Type u_1} {a : α} {l : List α} :
          (a :: l).tail! = l

          partitionM #

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

          Monadic generalization of List.partition.

          This uses Array.toList and which isn't imported by Init.Data.List.Basic or Init.Data.List.Control.

          def posOrNeg (x : Int) : Except String Bool :=
            if x > 0 then pure true
            else if x < 0 then pure false
            else throw "Zero is not positive or negative"
          
          partitionM posOrNeg [-1, 2, 3] = Except.ok ([2, 3], [-1])
          partitionM posOrNeg [0, 2, 3] = Except.error "Zero is not positive or negative"
          
          Equations
          Instances For
            @[specialize #[]]
            def List.partitionM.go {m : TypeType u_1} {α : Type} [Monad m] (p : αm Bool) :
            List αArray αArray αm (List α × List α)

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

            Equations
            Instances For

              partitionMap #

              @[inline]
              def List.partitionMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβ γ) (l : List α) :
              List β × List γ

              Given a function f : α → β ⊕ γ, partitionMap f l maps the list by f whilst partitioning the result into a pair of lists, List β × List γ, partitioning the .inl _ into the left list, and the .inr _ into the right List.

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

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

                Equations
                Instances For

                  mapMono #

                  This is a performance optimization for List.mapM that avoids allocating a new list when the result of each f a is a pointer equal value a.

                  For verification purposes, List.mapMono = List.map.

                  @[implemented_by _private.Init.Data.List.BasicAux.0.List.mapMonoMImp]
                  def List.mapMonoM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (as : List α) (f : αm α) :
                  m (List α)

                  Monomorphic List.mapM. The internal implementation uses pointer equality, and does not allocate a new list if the result of each f a is a pointer equal value a.

                  Equations
                  • [].mapMonoM f = pure []
                  • (a :: as_1).mapMonoM f = do let __do_liftf a let __do_lift_1as_1.mapMonoM f pure (__do_lift :: __do_lift_1)
                  Instances For
                    def List.mapMono {α : Type u_1} (as : List α) (f : αα) :
                    List α
                    Equations
                    • as.mapMono f = (as.mapMonoM f).run
                    Instances For

                      Additional lemmas required for bootstrapping Array. #

                      theorem List.getElem_append_left {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : i < as.length) {h' : i < (as ++ bs).length} :
                      (as ++ bs)[i] = as[i]
                      theorem List.getElem_append_right {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : ¬i < as.length) {h' : i < (as ++ bs).length} {h'' : i - as.length < bs.length} :
                      (as ++ bs)[i] = bs[i - as.length]
                      theorem List.get_last {α : Type u_1} {a : α} {as : List α} {i : Fin (as ++ [a]).length} (h : ¬i < as.length) :
                      (as ++ [a]).get i = a
                      theorem List.sizeOf_lt_of_mem {α : Type u_1} {a : α} [SizeOf α] {as : List α} (h : a as) :

                      This tactic, added to the decreasing_trivial toolbox, proves that sizeOf a < sizeOf as when a ∈ as, which is useful for well founded recursions over a nested inductive like inductive T | mk : List T → T.

                      Equations
                      Instances For
                        theorem List.append_cancel_left {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = as ++ cs) :
                        bs = cs
                        theorem List.append_cancel_right {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = cs ++ bs) :
                        as = cs
                        @[simp]
                        theorem List.append_cancel_left_eq {α : Type u_1} (as : List α) (bs : List α) (cs : List α) :
                        (as ++ bs = as ++ cs) = (bs = cs)
                        @[simp]
                        theorem List.append_cancel_right_eq {α : Type u_1} (as : List α) (bs : List α) (cs : List α) :
                        (as ++ bs = cs ++ bs) = (as = cs)
                        @[simp]
                        theorem List.sizeOf_get {α : Type u_1} [SizeOf α] (as : List α) (i : Fin as.length) :
                        sizeOf (as.get i) < sizeOf as
                        theorem List.le_antisymm {α : Type u_1} [LT α] [s : Antisymm fun (x x_1 : α) => ¬x < x_1] {as : List α} {bs : List α} (h₁ : as bs) (h₂ : bs as) :
                        as = bs
                        instance List.instAntisymmLeOfNotLt {α : Type u_1} [LT α] [Antisymm fun (x x_1 : α) => ¬x < x_1] :
                        Antisymm fun (x x_1 : List α) => x x_1
                        Equations
                        • List.instAntisymmLeOfNotLt = { antisymm := }