Documentation

Init.Data.List.BasicAux

source
def List.get! {α : Type u_1} [inst : Inhabited α] :
List α → Nat → α
Equations
source
def List.get? {α : Type u_1} :
List α → Nat → Option α
Equations
source
def List.getD {α : Type u_1} (as : List α) (idx : Nat) (a₀ : α) :
α
Equations
source
def List.head! {α : Type u_1} [inst : Inhabited α] :
List α → α
Equations
source
def List.head? {α : Type u_1} :
List α → Option α
Equations
source
def List.headD {α : Type u_1} :
List α → α → α
Equations
  • List.headD _fun_discr _fun_discr = match _fun_discr, _fun_discr with | [], a₀ => a₀ | a :: tail, x => a
source
def List.head {α : Type u_1} (as : List α) :
as ≠ [] → α
Equations
  • List.head _fun_discr _fun_discr = match _fun_discr, _fun_discr with | a :: tail, x => a
source
def List.tail! {α : Type u_1} :
List α → List α
Equations
source
def List.tail? {α : Type u_1} :
List α → Option (List α)
Equations
source
def List.tailD {α : Type u_1} :
List α → List α → List α
Equations
  • List.tailD _fun_discr _fun_discr = match _fun_discr, _fun_discr with | [], as₀ => as₀ | head :: as, x => as
source
def List.getLast {α : Type u_1} (as : List α) :
as ≠ [] → α
Equations
source
def List.getLast! {α : Type u_1} [inst : Inhabited α] :
List α → α
Equations
source
def List.getLast? {α : Type u_1} :
List α → Option α
Equations
source
def List.getLastD {α : Type u_1} :
List α → α → α
Equations
source
def List.rotateLeft {α : Type u_1} (xs : List α) (n : optParam Nat 1) :
List α
Equations
source
def List.rotateRight {α : Type u_1} (xs : List α) (n : optParam Nat 1) :
List α
Equations
source
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 }
source
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'' }
source
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
source
theorem List.sizeOf_lt_of_mem {α : Type u_1} {a : α} [inst : SizeOf α] {as : List α} (h : a ∈ as) :
sizeOf a < sizeOf as
source
def List.tacticSizeOf_list_dec :
Lean.ParserDescr
Equations
source
theorem List.append_cancel_left {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = as ++ cs) :
bs = cs
source
theorem List.append_cancel_right {α : Type u_1} {as : List α} {bs : List α} {cs : List α} (h : as ++ bs = cs ++ bs) :
as = cs
source
@[simp]
theorem List.append_cancel_left_eq {α : Type u_1} (as : List α) (bs : List α) (cs : List α) :
(as ++ bs = as ++ cs) = (bs = cs)
source
@[simp]
theorem List.append_cancel_right_eq {α : Type u_1} (as : List α) (bs : List α) (cs : List α) :
(as ++ bs = cs ++ bs) = (as = cs)
source
@[simp]
theorem List.sizeOf_get {α : Type u_1} [inst : SizeOf α] (as : List α) (i : Fin (List.length as)) :
sizeOf (List.get as i) < sizeOf as
source
theorem List.le_antisymm {α : Type u_1} [inst : LT α] [s : Antisymm fun a a_1 => ¬a < a_1] {as : List α} {bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) :
as = bs
source
instance List.instAntisymmListLeInstLEList {α : Type u_1} [inst : LT α] [inst : Antisymm fun a a_1 => ¬a < a_1] :
Antisymm fun a a_1 => a ≤ a_1
Equations
  • List.instAntisymmListLeInstLEList = { antisymm := (_ : ∀ {a b : List α}, a ≤ b → b ≤ a → a = b) }