Init.Data.List.Basic

List.replace [] _fun_discr _fun_discr = []
List.replace (a :: as) _fun_discr _fun_discr = match a == _fun_discr with | true => _fun_discr :: as | false => a :: List.replace as _fun_discr _fun_discr

source

def List.elem {α : Type u} [inst : BEq α] (a : α) :

List α → Bool

Equations

List.elem a [] = false
List.elem a (head :: tail) = match a == head with | true => true | false => List.elem a tail

source

def List.notElem {α : Type u} [inst : BEq α] (a : α) (as : List α) :

Bool

Equations

List.notElem a as = !List.elem a as

source

@[inline]

abbrev List.contains {α : Type u} [inst : BEq α] (as : List α) (a : α) :

Bool

Equations

List.contains as a = List.elem a as

source

inductive List.Mem {α : Type u} :

α → List α → Prop

head: ∀ {α : Type u} (a : α) (as : List α), List.Mem a (a :: as)
tail: ∀ {α : Type u} (a : α) {b : α} {as : List α}, List.Mem b as → List.Mem b (a :: as)

source

instance List.instMembershipList {α : Type u} :

Membership α (List α)

Equations

List.instMembershipList = { mem := List.Mem }

source

theorem List.mem_of_elem_eq_true {α : Type u} [inst : DecidableEq α] {a : α} {as : List α} :

∀ (a : List.elem a as = true), a ∈ as

source

theorem List.elem_eq_true_of_mem {α : Type u} [inst : DecidableEq α] {a : α} {as : List α} (h : a ∈ as) :

List.elem a as = true

source

instance List.instDecidableMemListInstMembershipList {α : Type u} [inst : DecidableEq α] (a : α) (as : List α) :

Decidable (a ∈ as)

Equations

List.instDecidableMemListInstMembershipList a as = decidable_of_decidable_of_iff (_ : List.elem a as = true ↔ a ∈ as)

source

theorem List.mem_append_of_mem_left {α : Type u} {a : α} {as : List α} (bs : List α) :

∀ (a : a ∈ as), a ∈ as ++ bs

source

theorem List.mem_append_of_mem_right {α : Type u} {b : α} {bs : List α} (as : List α) :

b ∈ bs → b ∈ as ++ bs

source

def List.eraseDupsAux {α : Type u_1} [inst : BEq α] :

List α → List α → List α

Equations

List.eraseDupsAux [] _fun_discr = List.reverse _fun_discr
List.eraseDupsAux (a :: l) _fun_discr = match List.elem a _fun_discr with | true => List.eraseDupsAux l _fun_discr | false => List.eraseDupsAux l (a :: _fun_discr)

source

def List.eraseDups {α : Type u_1} [inst : BEq α] (as : List α) :

List α

Equations

List.eraseDups as = List.eraseDupsAux as []

source

def List.eraseRepsAux {α : Type u_1} [inst : BEq α] :

α → List α → List α → List α

Equations

List.eraseRepsAux _fun_discr [] _fun_discr = List.reverse (_fun_discr :: _fun_discr)
List.eraseRepsAux _fun_discr (a' :: as) _fun_discr = match _fun_discr == a' with | true => List.eraseRepsAux _fun_discr as _fun_discr | false => List.eraseRepsAux a' as (_fun_discr :: _fun_discr)

source

def List.eraseReps {α : Type u_1} [inst : BEq α] :

List α → List α

Equations

List.eraseReps _fun_discr = match _fun_discr with | [] => [] | a :: as => List.eraseRepsAux a as []

Erase repeated adjacent elements.

source

@[specialize]

def List.spanAux {α : Type u} (p : α → Bool) :

List α → List α → List α × List α

Equations

List.spanAux p [] _fun_discr = (List.reverse _fun_discr, [])
List.spanAux p (a :: l) _fun_discr = match p a with | true => List.spanAux p l (a :: _fun_discr) | false => (List.reverse _fun_discr, a :: l)

source

@[inline]

def List.span {α : Type u} (p : α → Bool) (as : List α) :

List α × List α

Equations

List.span p as = List.spanAux p as []

source

@[specialize]

def List.groupByAux {α : Type u} (eq : α → α → Bool) :

List α → List (List α) → List (List α)

Equations

List.groupByAux eq (a :: as) ((ag :: g) :: gs) = match eq a ag with | true => List.groupByAux eq as ((a :: ag :: g) :: gs) | false => List.groupByAux eq as ([a] :: List.reverse (ag :: g) :: gs)
List.groupByAux eq _fun_discr _fun_discr = List.reverse _fun_discr

source

@[specialize]

def List.groupBy {α : Type u} (p : α → α → Bool) :

List α → List (List α)

Equations

List.groupBy p _fun_discr = match _fun_discr with | [] => [] | a :: as => List.groupByAux p as [[a]]

source

def List.lookup {α : Type u} {β : Type v} [inst : BEq α] :

α → List (α × β) → Option β

Equations

List.lookup _fun_discr [] = none
List.lookup _fun_discr ((k, b) :: es) = match _fun_discr == k with | true => some b | false => List.lookup _fun_discr es

source

def List.removeAll {α : Type u} [inst : BEq α] (xs : List α) (ys : List α) :

List α

Equations

List.removeAll xs ys = List.filter (fun x => List.notElem x ys) xs

source

def List.drop {α : Type u} :

Nat → List α → List α

Equations

List.drop 0 _fun_discr = _fun_discr
List.drop (Nat.succ n) [] = []
List.drop (Nat.succ n) (head :: as) = List.drop n as

source

def List.take {α : Type u} :

Nat → List α → List α

Equations

List.take 0 _fun_discr = []
List.take (Nat.succ n) [] = []
List.take (Nat.succ n) (head :: as) = head :: List.take n as

source

def List.takeWhile {α : Type u} (p : α → Bool) :

List α → List α

Equations

List.takeWhile p [] = []
List.takeWhile p (head :: tail) = match p head with | true => head :: List.takeWhile p tail | false => []

source

@[specialize]

def List.foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) :

List α → β

Equations

List.foldr f init [] = init
List.foldr f init (head :: tail) = f head (List.foldr f init tail)

source

@[inline]

def List.any {α : Type u} (l : List α) (p : α → Bool) :

Bool

Equations

List.any l p = List.foldr (fun a r => p a || r) false l

source

@[inline]

def List.all {α : Type u} (l : List α) (p : α → Bool) :

Bool

Equations

List.all l p = List.foldr (fun a r => p a && r) true l

source

def List.or (bs : List Bool) :

Bool

Equations

List.or bs = List.any bs id

source

def List.and (bs : List Bool) :

Bool

Equations

List.and bs = List.all bs id

source

def List.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) :

List α → List β → List γ

Equations

List.zipWith f (x :: xs) (y :: ys) = f x y :: List.zipWith f xs ys
List.zipWith f _fun_discr _fun_discr = []

source

def List.zip {α : Type u} {β : Type v} :

List α → List β → List (α × β)

Equations

List.zip = List.zipWith Prod.mk

source

def List.unzip {α : Type u} {β : Type v} :

List (α × β) → List α × List β

Equations

List.unzip [] = ([], [])
List.unzip ((a, b) :: t) = (a :: (List.unzip t).1, b :: (List.unzip t).2)

source

def List.rangeAux :

Nat → List Nat → List Nat

Equations

List.rangeAux 0 _fun_discr = _fun_discr
List.rangeAux (Nat.succ n) _fun_discr = List.rangeAux n (n :: _fun_discr)

source

def List.range (n : Nat) :

List Nat

Equations

List.range n = List.rangeAux n []

source

def List.iota :

Nat → List Nat

Equations

List.iota 0 = []
List.iota (Nat.succ n) = Nat.succ n :: List.iota n

source

def List.iotaTR (n : Nat) :

List Nat

Equations

List.iotaTR n = List.iotaTR.go n []

source

def List.iotaTR.go :

Nat → List Nat → List Nat

Equations

List.iotaTR.go 0 _fun_discr = List.reverse _fun_discr
List.iotaTR.go (Nat.succ n) _fun_discr = List.iotaTR.go n (Nat.succ n :: _fun_discr)

source

theorem List.iota_eq_iotaTR :

List.iota = List.iotaTR

source

def List.enumFrom {α : Type u} :

Nat → List α → List (Nat × α)

Equations

List.enumFrom _fun_discr [] = []
List.enumFrom _fun_discr (x :: xs) = (_fun_discr, x) :: List.enumFrom (_fun_discr + 1) xs

source

def List.enum {α : Type u} :

List α → List (Nat × α)

Equations

List.enum = List.enumFrom 0

source

def List.init {α : Type u} :

List α → List α

Equations

List.init [] = []
List.init [head] = []
List.init (a :: l) = a :: List.init l

source

def List.intersperse {α : Type u} (sep : α) :

List α → List α

Equations

List.intersperse sep [] = []
List.intersperse sep [head] = [head]
List.intersperse sep (a :: l) = a :: sep :: List.intersperse sep l

source

def List.intercalate {α : Type u} (sep : List α) (xs : List (List α)) :

List α

Equations

List.intercalate sep xs = List.join (List.intersperse sep xs)

source

@[inline]

def List.bind {α : Type u} {β : Type v} (a : List α) (b : α → List β) :

List β

Equations

List.bind a b = List.join (List.map b a)

source

@[inline]

def List.pure {α : Type u} (a : α) :

List α

Equations

List.pure a = [a]

source

inductive List.lt {α : Type u} [inst : LT α] :

List α → List α → Prop

nil: ∀ {α : Type u} [inst : LT α] (b : α) (bs : List α), List.lt [] (b :: bs)
head: ∀ {α : Type u} [inst : LT α] {a : α} (as : List α) {b : α} (bs : List α), a < b → List.lt (a :: as) (b :: bs)
tail: ∀ {α : Type u} [inst : LT α] {a : α} {as : List α} {b : α} {bs : List α}, ¬a < b → ¬b < a → List.lt as bs → List.lt (a :: as) (b :: bs)

source

instance List.instLTList {α : Type u} [inst : LT α] :

LT (List α)

Equations

List.instLTList = { lt := List.lt }

source

instance List.hasDecidableLt {α : Type u} [inst : LT α] [h : DecidableRel fun a a_1 => a < a_1] (l₁ : List α) (l₂ : List α) :

Decidable (l₁ < l₂)

Equations

List.hasDecidableLt [] [] = isFalse (_ : [] < [] → False)
List.hasDecidableLt [] (head :: tail) = isTrue (_ : List.lt [] (head :: tail))
List.hasDecidableLt (head :: tail) [] = isFalse (_ : head :: tail < [] → False)
List.hasDecidableLt (a :: as) (b :: bs) = match h a b with | isTrue h₁ => isTrue (_ : List.lt (a :: as) (b :: bs)) | isFalse h₁ => match h b a with | isTrue h₂ => isFalse (_ : a :: as < b :: bs → False) | isFalse h₂ => match List.hasDecidableLt as bs with | isTrue h₃ => isTrue (_ : List.lt (a :: as) (b :: bs)) | isFalse h₃ => isFalse (_ : a :: as < b :: bs → False)

source

noncomputable def List.le {α : Type u} [inst : LT α] (a : List α) (b : List α) :

Prop

Equations

List.le a b = ¬b < a

source

instance List.instLEList {α : Type u} [inst : LT α] :

LE (List α)

Equations

List.instLEList = { le := List.le }

source

instance List.instForAllListDecidableLeInstLEList {α : Type u} [inst : LT α] [inst : DecidableRel fun a a_1 => a < a_1] (l₁ : List α) (l₂ : List α) :

Decidable (l₁ ≤ l₂)

Equations

List.instForAllListDecidableLeInstLEList x x = inferInstanceAs (Decidable ¬x < x)

source

def List.isPrefixOf {α : Type u} [inst : BEq α] :

List α → List α → Bool

Equations

List.isPrefixOf [] _fun_discr = true
List.isPrefixOf _fun_discr [] = false
List.isPrefixOf (a :: as) (b :: bs) = (a == b && List.isPrefixOf as bs)

isPrefixOfl₁l₂ returns true Iff l₁ is a prefix of l₂.

source

def List.isSuffixOf {α : Type u} [inst : BEq α] (l₁ : List α) (l₂ : List α) :

Bool

Equations

List.isSuffixOf l₁ l₂ = List.isPrefixOf (List.reverse l₁) (List.reverse l₂)

isSuffixOfl₁l₂ returns true Iff l₁ is a suffix of l₂.

source

@[specialize]

def List.isEqv {α : Type u} :

List α → List α → (α → α → Bool) → Bool

Equations

List.isEqv [] [] _fun_discr = true
List.isEqv (a :: as) (b :: bs) _fun_discr = (_fun_discr a b && List.isEqv as bs _fun_discr)
List.isEqv _fun_discr _fun_discr _fun_discr = false