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.

def List.get! {α : Type u_1} [Inhabited α] :
List αNatα
Equations
Instances For
    def List.get? {α : Type u_1} :
    List αNatOption α
    Equations
    Instances For
      def List.getD {α : Type u_1} (as : List α) (idx : Nat) (a₀ : α) :
      α
      Equations
      Instances For
        def List.head! {α : Type u_1} [Inhabited α] :
        List αα
        Equations
        Instances For
          def List.head? {α : Type u_1} :
          List αOption α
          Equations
          Instances For
            def List.headD {α : Type u_1} :
            List ααα
            Equations
            • List.headD x✝ x = match x✝, x with | [], a₀ => a₀ | a :: tail, x => a
            Instances For
              def List.head {α : Type u_1} (as : List α) :
              as []α
              Equations
              Instances For
                def List.tail! {α : Type u_1} :
                List αList α
                Equations
                Instances For
                  def List.tail? {α : Type u_1} :
                  List αOption (List α)
                  Equations
                  Instances For
                    def List.tailD {α : Type u_1} :
                    List αList αList α
                    Equations
                    • List.tailD x✝ x = match x✝, x with | [], as₀ => as₀ | head :: as, x => as
                    Instances For
                      def List.getLast {α : Type u_1} (as : List α) :
                      as []α
                      Equations
                      Instances For
                        def List.getLast! {α : Type u_1} [Inhabited α] :
                        List αα
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def List.getLast? {α : Type u_1} :
                          List αOption α
                          Equations
                          Instances For
                            def List.getLastD {α : Type u_1} :
                            List ααα
                            Equations
                            Instances For
                              def List.rotateLeft {α : Type u_1} (xs : List α) (n : optParam Nat 1) :
                              List α
                              Equations
                              Instances For
                                def List.rotateRight {α : Type u_1} (xs : List α) (n : optParam Nat 1) :
                                List α
                                Equations
                                Instances For
                                  theorem List.get_append_left {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : i < List.length as) {h' : i < List.length (as ++ bs)} :
                                  List.get (as ++ bs) { val := i, isLt := h' } = List.get as { val := i, isLt := h }
                                  theorem List.get_append_right {α : Type u_1} {i : Nat} (as : List α) (bs : List α) (h : ¬i < List.length as) {h' : i < List.length (as ++ bs)} {h'' : i - List.length as < List.length bs} :
                                  List.get (as ++ bs) { val := i, isLt := h' } = List.get bs { val := i - List.length as, isLt := h'' }
                                  theorem List.get_last {α : Type u_1} {a : α} {as : List α} {i : Fin (List.length (as ++ [a]))} (h : ¬i.val < List.length as) :
                                  List.get (as ++ [a]) 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 (List.length 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.instAntisymmListLeInstLEList {α : Type u_1} [LT α] [Antisymm fun (x x_1 : α) => ¬x < x_1] :
                                    Antisymm fun (x x_1 : List α) => x x_1
                                    Equations
                                    • List.instAntisymmListLeInstLEList = { antisymm := (_ : ∀ {a b : List α}, a bb aa = b) }
                                    @[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
                                    Instances For
                                      def List.mapMono {α : Type u_1} (as : List α) (f : αα) :
                                      List α
                                      Equations
                                      Instances For