mathlib documentation

data.equiv.list

def encodable.decode_list {α : Type u_1} [encodable α] :
option (list α)

Equations
@[instance]
def encodable.list {α : Type u_1} [encodable α] :

Equations
@[simp]
theorem encodable.encode_list_nil {α : Type u_1} [encodable α] :

@[simp]
theorem encodable.encode_list_cons {α : Type u_1} [encodable α] (a : α) (l : list α) :

@[simp]
theorem encodable.decode_list_zero {α : Type u_1} [encodable α] :

@[simp]
theorem encodable.decode_list_succ {α : Type u_1} [encodable α] (v : ) :
encodable.decode (list α) v.succ = (λ (_x : α) (_y : list α), _x :: _y) <$> encodable.decode α v.unpair.fst <*> encodable.decode (list α) v.unpair.snd

theorem encodable.length_le_encode {α : Type u_1} [encodable α] (l : list α) :

@[instance]
def encodable.multiset {α : Type u_1} [encodable α] :

Equations
def encodable.encodable_of_list {α : Type u_1} [decidable_eq α] (l : list α) :
(∀ (x : α), x l)encodable α

Equations
@[instance]
def encodable.vector {α : Type u_1} [encodable α] {n : } :

Equations
@[instance]
def encodable.fin_arrow {α : Type u_1} [encodable α] {n : } :
encodable (fin n → α)

Equations
@[instance]
def encodable.fin_pi (n : ) (π : fin nType u_1) [Π (i : fin n), encodable («π» i)] :
encodable (Π (i : fin n), «π» i)

Equations
@[instance]
def encodable.array {α : Type u_1} [encodable α] {n : } :

Equations
@[instance]
def encodable.finset {α : Type u_1} [encodable α] :

Equations
def encodable.fintype_arrow (α : Type u_1) (β : Type u_2) [decidable_eq α] [fintype α] [encodable β] :
trunc (encodable (α → β))

Equations
def encodable.fintype_pi (α : Type u_1) (π : α → Type u_2) [decidable_eq α] [fintype α] [Π (a : α), encodable («π» a)] :
trunc (encodable (Π (a : α), «π» a))

Equations
def encodable.sorted_univ (α : Type u_1) [fintype α] [encodable α] :
list α

The elements of a fintype as a sorted list.

Equations
theorem encodable.mem_sorted_univ {α : Type u_1} [fintype α] [encodable α] (x : α) :

def encodable.fintype_equiv_fin {α : Type u_1} [fintype α] [encodable α] :

An encodable fintype is equivalent a fin.

Equations
theorem denumerable.denumerable_list_aux {α : Type u_1} [denumerable α] (n : ) :

@[simp]

theorem denumerable.raise_lower' {l : list } {n : } :
(∀ (m : ), m ln m)list.sorted has_lt.lt ldenumerable.raise' (denumerable.lower' l n) n = l

The type lists on unit is canonically equivalent to the natural numbers.

Equations