Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Authors: Leonardo de Moura
-/
import Mathlib.Mathport.Rename
import Mathlib.Init.Data.Nat.Notation
import Std.Data.Nat.Lemmas
import Std.Data.List.Basic
/-!
Definitions for `List` not (yet) in `Std`
-/

open Decidable List

universe u v w

namespace List

open Option Nat

#align list.nth
List.get?: {α : Type u_1} → List α
List.get?
/-- nth element of a list `l` given `n < l.length`. -/ @[deprecated
get: {α : Type u} → (as : List α) → Fin (length as)α
get
] def
nthLe: {α : Type u_1} → (l : List α) → (n : ) → n < α
nthLe
(
l: List α
l
:
List: Type ?u.7 → Type ?u.7
List
α: ?m.4
α
) (
n:
n
) (
h: n <
h
:
n: ?m.10
n
<
l: List α
l
.
length: {α : Type ?u.14} → List α
length
) :
α: ?m.4
α
:=
get: {α : Type ?u.30} → (as : List α) → Fin (length as)α
get
l: List α
l
n:
n
,
h: n <
h
#align list.nth_le
List.nthLe: {α : Type u_1} → (l : List α) → (n : ) → n < α
List.nthLe
set_option linter.deprecated false in @[deprecated] theorem
nthLe_eq: ∀ {α : Type u_1} (l : List α) (n : ) (h : n < ), nthLe l n h = get l { val := n, isLt := h }
nthLe_eq
(
l: List α
l
:
List: Type ?u.117 → Type ?u.117
List
α: ?m.114
α
) (
n: ?m.120
n
) (
h: n <
h
:
n: ?m.120
n
<
l: List α
l
.
length: {α : Type ?u.124} → List α
length
) :
nthLe: {α : Type ?u.136} → (l : List α) → (n : ) → n < α
nthLe
l: List α
l
n: ?m.120
n
h: n <
h
=
get: {α : Type ?u.139} → (as : List α) → Fin (length as)α
get
l: List α
l
n: ?m.120
n
,
h: n <
h
⟩ :=
rfl: ∀ {α : Sort ?u.153} {a : α}, a = a
rfl
/-- The head of a list, or the default element of the type is the list is `nil`. -/ def
headI: {α : Type ?u.185} → [inst : ] → List αα
[
Inhabited: Sort ?u.181 → Sort (max1?u.181)
Inhabited
α: ?m.178
α
] :
List: Type ?u.185 → Type ?u.185
List
α: ?m.178
α
α: ?m.178
α
| [] =>
default: {α : Sort ?u.203} → [self : ] → α
default
| (
a: α
a
:: _) =>
a: α
a
List.headI: {α : Type u_1} → [inst : ] → List αα
@[simp] theorem
headI_nil: ∀ {α : Type u_1} [inst : ], headI [] = default
[
Inhabited: Sort ?u.502 → Sort (max1?u.502)
Inhabited
α: ?m.499
α
] : (
[]: List ?m.509
[]
:
List: Type ?u.507 → Type ?u.507
List
α: ?m.499
α
).
headI: {α : Type ?u.511} → [inst : ] → List αα
=
default: {α : Sort ?u.522} → [self : ] → α
default
:=
rfl: ∀ {α : Sort ?u.696} {a : α}, a = a
rfl
@[simp] theorem
headI_cons: ∀ {α : Type u_1} [inst : ] {h : α} {t : List α}, headI (h :: t) = h
[
Inhabited: Sort ?u.727 → Sort (max1?u.727)
Inhabited
α: ?m.724
α
] {
h: α
h
:
α: ?m.724
α
} {
t: List α
t
:
List: Type ?u.732 → Type ?u.732
List
α: ?m.724
α
} : (
h: α
h
::
t: List α
t
).
headI: {α : Type ?u.739} → [inst : ] → List αα
=
h: α
h
:=
rfl: ∀ {α : Sort ?u.756} {a : α}, a = a
rfl
#align list.map₂
List.zipWith: {α : Type u} → {β : Type v} → {γ : Type w} → (αβγ) → List αList βList γ
List.zipWith
#noalign list.map_with_index_core #align list.map_with_index
List.mapIdx: {α : Type u_1} → {β : Type u_2} → (αβ) → List αList β
List.mapIdx
/-- Find index of element with given property. -/ @[deprecated
findIdx: {α : Type u_1} → (αBool) → List α
findIdx
] def
findIndex: {α : Type u_1} → (p : αProp) → [inst : ] → List α
findIndex
(
p: αProp
p
:
α: ?m.792
α
Prop: Type
Prop
) [
DecidablePred: {α : Sort ?u.799} → (αProp) → Sort (max1?u.799)
DecidablePred
p: αProp
p
] :
List: Type ?u.810 → Type ?u.810
List
α: ?m.792
α
: Type
:=
List.findIdx: {α : Type ?u.817} → (αBool) → List α
List.findIdx
p: αProp
p
#align list.find_index
List.findIndex: {α : Type u_1} → (p : αProp) → [inst : ] → List α
List.findIndex
#align list.update_nth
List.set: {α : Type u_1} → List ααList α
List.set
#align list.bor
List.or:
List.or
#align list.band
List.and:
List.and
#align list.last
List.getLast: {α : Type u_1} → (as : List α) → as []α
List.getLast
/-- The last element of a list, with the default if list empty -/ def
getLastI: {α : Type ?u.959} → [inst : ] → List αα
getLastI
[
Inhabited: Sort ?u.955 → Sort (max1?u.955)
Inhabited
α: ?m.952
α
] :
List: Type ?u.959 → Type ?u.959
List
α: ?m.952
α
α: ?m.952
α
| [] =>
default: {α : Sort ?u.977} → [self : ] → α
default
| [
a: α
a
] =>
a: α
a
| [_,
b: α
b
] =>
b: α
b
| _ :: _ ::
l: List α
l
=>
getLastI: {α : Type ?u.959} → [inst : ] → List αα
getLastI
l: List α
l
#align list.ilast
List.getLastI: {α : Type u_1} → [inst : ] → List αα
List.getLastI
#align list.init
List.dropLast: {α : Type u_1} → List αList α
List.dropLast
/-- List with a single given element. -/ @[inline] protected def
ret: {α : Type u} → αList α
ret
{
α: Type u
α
:
Type u: Type (u+1)
Type u
} (
a: α
a
:
α: Type u
α
) :
List: Type ?u.1717 → Type ?u.1717
List
α: Type u
α
:= [
a: α
a
] #align list.ret
List.ret: {α : Type u} → αList α
List.ret
/-- `≤` implies not `>` for lists. -/ theorem
le_eq_not_gt: ∀ {α : Type u_1} [inst : LT α] (l₁ l₂ : List α), (l₁ l₂) = ¬l₂ < l₁
le_eq_not_gt
[
LT: Type ?u.1757 → Type ?u.1757
LT
α: ?m.1754
α
] : ∀
l₁: List α
l₁
l₂: List α
l₂
:
List: Type ?u.1761 → Type ?u.1761
List
α: ?m.1754
α
, (
l₁: List α
l₁
l₂: List α
l₂
) = ¬
l₂: List α
l₂
<
l₁: List α
l₁
:= fun
_: ?m.1793
_
_: ?m.1796
_
=>
rfl: ∀ {α : Sort ?u.1798} {a : α}, a = a
rfl
#align list.le_eq_not_gt
List.le_eq_not_gt: ∀ {α : Type u_1} [inst : LT α] (l₁ l₂ : List α), (l₁ l₂) = ¬l₂ < l₁
List.le_eq_not_gt
end List #align list.replicate
List.replicate: {α : Type u} → αList α
List.replicate
#align list.length_replicate
List.length_replicate: ∀ {α : Type u} (n : ) (a : α), length () = n
List.length_replicate