Equivalences involving List
-like types #
This file defines some additional constructive equivalences using Encodable
and the pairing
function on ℕ
.
@[simp]
theorem
Encodable.decode_list_succ
{α : Type u_1}
[Encodable α]
(v : ℕ)
:
decode v.succ = (fun (x1 : α) (x2 : List α) => x1 :: x2) <$> decode (Nat.unpair v).1 <*> decode (Nat.unpair v).2
These two lemmas are not about lists, but are convenient to keep here and don't
require Finset.sort
.
A listable type with decidable equality is encodable.
Equations
Instances For
A finite type is encodable. Because the encoding is not unique, we wrap it in Trunc
to
preserve computability.
Equations
Instances For
A noncomputable way to arbitrarily choose an ordering on a finite type.
It is not made into a global instance, since it involves an arbitrary choice.
This can be locally made into an instance with attribute [local instance] Fintype.toEncodable
.
Equations
Instances For
@[irreducible]
theorem
Denumerable.denumerable_list_aux
{α : Type u_1}
[Denumerable α]
(n : ℕ)
:
∃ a ∈ Encodable.decodeList n, Encodable.encodeList a = n
If α
is denumerable, then so is List α
.
Equations
@[simp]
@[simp]
@[simp]
@[simp]