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
    • [].getLast! = panicWithPosWithDecl "Init.Data.List.BasicAux" "List.getLast!" 44 13 "empty list"
    • (a :: as).getLast! = (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
      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
        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} {as : List α} {bs : List α} {i : Nat} (h₁ : as.length i) {h₂ : i < (as ++ 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)
                        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 (x1 x2 : α) => ¬x1 < x2] {as : List α} {bs : List α} (h₁ : as bs) (h₂ : bs as) :
                        as = bs
                        instance List.instAntisymmLeOfNotLt {α : Type u_1} [LT α] [Antisymm fun (x1 x2 : α) => ¬x1 < x2] :
                        Antisymm fun (x1 x2 : List α) => x1 x2
                        Equations
                        • =