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 x x = match x, x with | [], a₀ => a₀ | a :: x, x_1 => a
source
def List.head {α : Type u_1} (as : List α) :
as ≠ [] → α
Equations
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 x x = match x, x with | [], as₀ => as₀ | a :: 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