/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 α → ℕ → Option α
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 < length l → α
nthLe (l: List α
l : List: Type ?u.7 → Type ?u.7
List α: ?m.4
α) (n: ℕ
n) (h: n < length l
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 < length l
h⟩
#align list.nth_le List.nthLe: {α : Type u_1} → (l : List α) → (n : ℕ) → n < length l → α
List.nthLe

set_option linter.deprecated false in
@[deprecated]
theorem nthLe_eq: ∀ {α : Type u_1} (l : List α) (n : ℕ) (h : n < length l), 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 < length l
h : n: ?m.120
n < l: List α
l.length: {α : Type ?u.124} → List α → ℕ
length) : nthLe: {α : Type ?u.136} → (l : List α) → (n : ℕ) → n < length l → α
nthLe l: List α
l n: ?m.120
n h: n < length l
h = get: {α : Type ?u.139} → (as : List α) → Fin (length as) → α
get l: List α
l ⟨n: ?m.120
n, h: n < length l
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 : Inhabited α] → List α → α
headI [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 : Inhabited α] → α
default
| (a: α
a :: _) => a: α
a
#align list.head List.headI: {α : Type u_1} → [inst : Inhabited α] → List α → α
List.headI

@[simp] theorem headI_nil: ∀ {α : Type u_1} [inst : Inhabited α], headI [] = default
headI_nil [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 : Inhabited α] → List α → α
headI = default: {α : Sort ?u.522} → [self : Inhabited α] → α
default := rfl: ∀ {α : Sort ?u.696} {a : α}, a = a
rfl
@[simp] theorem headI_cons: ∀ {α : Type u_1} [inst : Inhabited α] {h : α} {t : List α}, headI (h :: t) = h
headI_cons [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 : Inhabited α] → List α → α
headI = 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 : DecidablePred p] → 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 : DecidablePred p] → List α → ℕ
List.findIndex

#align list.update_nth List.set: {α : Type u_1} → List α → ℕ → α → List α
List.set

#align list.bor List.or: List Bool → Bool
List.or

#align list.band List.and: List Bool → Bool
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 : Inhabited α] → 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 : Inhabited α] → α
default
  | [a: α
a] => a: α
a
  | [_, b: α
b] => b: α
b
  | _ :: _ :: l: List α
l => getLastI: {α : Type ?u.959} → [inst : Inhabited α] → List α → α
getLastI l: List α
l
#align list.ilast List.getLastI: {α : Type u_1} → [inst : Inhabited α] → 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 (replicate n a) = n
List.length_replicate