def Nat.predO : ℕ → Option ℕ

Equations

• x.predO = match x with | 0 => none | n.succ => some n

@[simp]

theorem Nat.predO_zero : Nat.predO 0 = none

@[simp]

theorem Nat.predO_succ {n : ℕ} : (n + 1).predO = some n

def List.range2 (n : ℕ) (m : ℕ) : List (ℕ × ℕ)

Equations

• List.range2 n m = Seq.seq ((fun (x x_1 : ℕ) => (x, x_1)) <$> List.range n) fun (x : Unit) => List.range m

@[simp]

theorem List.mem_range2_iff {n : ℕ} {m : ℕ} {i : ℕ} {j : ℕ} : (i, j) ∈ List.range2 n m ↔ i < n ∧ j < m

def List.toVector {α : Type u_1} (n : ℕ) : List α → Option (Mathlib.Vector α n)

Equations

• List.toVector n l = if h : l.length = n then some ⟨l, h⟩ else none

def Encodable.fintypeArrowEquivFinArrow {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} : (ι → α) ≃ (Fin (Fintype.card ι) → α)

Equations

• Encodable.fintypeArrowEquivFinArrow = Encodable.fintypeEquivFin.arrowCongr (Equiv.refl α)

def Encodable.fintypeArrowEquivFinArrow' {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} {k : ℕ} (hk : Fintype.card ι = k) : (ι → α) ≃ (Fin k → α)

Equations

• Encodable.fintypeArrowEquivFinArrow' hk = hk ▸ Encodable.fintypeArrowEquivFinArrow

def Encodable.fintypeArrowEquivVector {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Type u_2} : (ι → α) ≃ Mathlib.Vector α (Fintype.card ι)

Equations

• Encodable.fintypeArrowEquivVector = Encodable.fintypeArrowEquivFinArrow.trans (Equiv.vectorEquivFin α (Fintype.card ι)).symm

theorem Encodable.fintypeArrowEquivFinArrow_eq {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} (f : ι → α) : Encodable.fintypeArrowEquivFinArrow f = fun (i : Fin (Fintype.card ι)) => f (Encodable.fintypeEquivFin.symm i)

@[simp]

theorem Encodable.fintypeArrowEquivFinArrow_app {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} (f : ι → α) (i : Fin (Fintype.card ι)) : Encodable.fintypeArrowEquivFinArrow f i = f (Encodable.fintypeEquivFin.symm i)

@[simp]

theorem Encodable.fintypeArrowEquivFinArrow_symm_app {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} {i : ι} (v : Fin (Fintype.card ι) → α) : Encodable.fintypeArrowEquivFinArrow.symm v i = v (Encodable.fintypeEquivFin i)

@[simp]

theorem Encodable.fintypeArrowEquivFinArrow'_app {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} {k : ℕ} (hk : Fintype.card ι = k) (f : ι → α) (i : Fin k) : (Encodable.fintypeArrowEquivFinArrow' hk) f i = f (Encodable.fintypeEquivFin.symm (Fin.cast ⋯ i))

@[simp]

theorem Encodable.fintypeArrowEquivFinArrow'_symm_app {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} {i : ι} {k : ℕ} (hk : Fintype.card ι = k) (v : Fin k → α) : (Encodable.fintypeArrowEquivFinArrow' hk).symm v i = v (Fin.cast hk (Encodable.fintypeEquivFin i))

@[simp]

theorem Encodable.cast_fintypeEquivFin_fin {k : ℕ} (i : Fin k) : Fin.cast ⋯ (Encodable.fintypeEquivFin i) = i

@[simp]

theorem Encodable.val_fintypeEquivFin_fin {k : ℕ} (i : Fin k) : ↑(Encodable.fintypeEquivFin i) = ↑i

@[simp]

theorem Encodable.fintypeEquivFin_false : Encodable.fintypeEquivFin false = 0

@[simp]

theorem Encodable.fintypeEquivFin_true : Encodable.fintypeEquivFin true = 1

@[simp]

theorem Encodable.fintypeEquivFin_symm_zero : Encodable.fintypeEquivFin.symm 0 = false

@[simp]

theorem Encodable.fintypeEquivFin_symm_one : Encodable.fintypeEquivFin.symm 1 = true

@[simp]

theorem Encodable.fintypeEquivFin_symm_cast_fin {k : ℕ} (i : Fin k) : Encodable.fintypeEquivFin.symm (Fin.cast ⋯ i) = i

@[simp]

theorem Encodable.fintypeArrowEquivFinArrow'_symm_app_fin_arrow {α : Sort u_2} {k : ℕ} (hk : Fintype.card (Fin k) = k) (v : Fin k → α) : (Encodable.fintypeArrowEquivFinArrow' hk).symm v = v

@[simp]

theorem Encodable.fintypeArrowEquivVector_app {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Type u_2} {i : Fin (Fintype.card ι)} (f : ι → α) : (Encodable.fintypeArrowEquivVector f).get i = f (Encodable.fintypeEquivFin.symm i)

@[simp]

theorem Encodable.fintypeArrowEquivVector_symm_app {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Type u_2} {i : ι} (v : Mathlib.Vector α (Fintype.card ι)) : Encodable.fintypeArrowEquivVector.symm v i = v.get (Encodable.fintypeEquivFin i)

@[simp]

theorem Encodable.fintypeArrowEquivFinArrow_fintypeEquivFin {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Sort u_2} (f : Fin (Fintype.card ι) → α) : (Encodable.fintypeArrowEquivFinArrow fun (i : ι) => f (Encodable.fintypeEquivFin i)) = f

def Encodable.toFinArrowOpt {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Type u_2} (f : ι → Option α) : Option (ι → α)

Equations

• Encodable.toFinArrowOpt f = Option.map (⇑Encodable.fintypeArrowEquivFinArrow.symm) (Matrix.toOptionVec (Encodable.fintypeArrowEquivFinArrow f))

@[simp]

theorem Encodable.toFinArrowOpt_eq_none_iff {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Type u_2} {f : ι → Option α} : Encodable.toFinArrowOpt f = none ↔ ∃ (i : ι), f i = none

@[simp]

theorem Encodable.toFinArrowOpt_eq_some_iff {ι : Type u_1} [Fintype ι] [Encodable ι] {α : Type u_2} {f : ι → Option α} {g : ι → α} : Encodable.toFinArrowOpt f = some g ↔ ∀ (i : ι), f i = some (g i)

@[simp]

theorem Encodable.vectorEquivFin_symm_val {n : ℕ} {β : Type u_2} (f : Fin n → β) : ((Equiv.vectorEquivFin β n).symm f).toList = List.ofFn f

@[simp]

def Encodable.getI_ofFn {α : Type u_2} [Inhabited α] {n : ℕ} (f : Fin n → α) (i : Fin n) : (List.ofFn f).getI ↑i = f i

Equations

• ⋯ = ⋯

@[reducible]

def Encodable.encodeDecode (α : Type u_2) [Encodable α] (e : ℕ) : Option ℕ

Equations

• Encodable.encodeDecode α e = (Encodable.encode (Encodable.decode e)).predO

theorem Encodable.encodeDecode_of_none {α : Type u_1} [Encodable α] {e : ℕ} (h : Encodable.decode e = none) : Encodable.encodeDecode α e = none

theorem Encodable.encodeDecode_of_some {α : Type u_1} [Encodable α] {e : ℕ} {a : α} (h : Encodable.decode e = some a) : Encodable.encodeDecode α e = some (Encodable.encode a)

theorem Encodable.encodeDecode_eq_encode_map_decode {α : Type u_1} [Encodable α] {e : ℕ} : Encodable.encodeDecode α e = Option.map Encodable.encode (Encodable.decode e)

theorem Encodable.decode_encodeDecode {α : Type u_1} [Encodable α] {e : ℕ} {i : ℕ} : Encodable.encodeDecode α e = some i → ∃ (a : α), Encodable.decode i = some a

theorem Encodable.encode_decode_subtype {α : Type u_1} {P : α → Prop} [Encodable α] [DecidablePred P] (e : ℕ) : Encodable.encode (Encodable.decode e) = Encodable.encode ((Encodable.decode e).bind fun (a : α) => if P a then some a else none)

theorem Encodable.encodeDecode_subtype' {α : Type u_1} {P : α → Prop} [Encodable α] [DecidablePred P] (e : ℕ) : Encodable.encodeDecode { x : α // P x } e = (Encodable.decode e).bind fun (a : α) => if P a then some (Encodable.encode a) else none

theorem Encodable.encodeDecode_subtype {α : Type u_1} {P : α → Prop} [Encodable α] [DecidablePred P] (e : ℕ) : Encodable.encodeDecode { x : α // P x } e = (Encodable.encodeDecode α e).bind fun (c : ℕ) => if ∃ a ∈ Encodable.decode c, P a then some c else none

theorem Encodable.encodeDecode_ofEquiv (α : Type u_2) [Encodable α] {β : Type u_3} (e : β ≃ α) : Encodable.encodeDecode β = Encodable.encodeDecode α

theorem Encodable.encodeDecode_ofEquiv_prim (α : Type u_2) {β : Type u_3} [Primcodable α] (e : β ≃ α) : Encodable.encodeDecode β = Encodable.encodeDecode α

theorem Encodable.encode_decode_eq_encodeDecode {α : Type u_1} [Encodable α] {e : ℕ} : Encodable.encode (Encodable.decode e) = Encodable.encode (Encodable.encodeDecode α e)

theorem Encodable.encode_decode_sigma_s {α : Type u_1} [Encodable α] {β : α → Type u_2} [(a : α) → Encodable (β a)] {e : ℕ} : Encodable.encodeDecode ((a : α) × β a) e = (Encodable.decode (Nat.unpair e).1).bind fun (a : α) => Option.map (fun (b : ℕ) => Nat.pair (Encodable.encode a) b) (Encodable.encodeDecode (β a) (Nat.unpair e).2)

theorem Encodable.encode_decode_sigma_of_none {α : Type u_1} [Encodable α] {β : α → Type u_2} [(a : α) → Encodable (β a)] {e : ℕ} (h : Encodable.decode (Nat.unpair e).1 = none) : Encodable.encodeDecode ((a : α) × β a) e = none

theorem Encodable.encode_decode_sigma_of_some {α : Type u_1} [Encodable α] {β : α → Type u_2} [(a : α) → Encodable (β a)] {e : ℕ} {a : α} (h : Encodable.decode (Nat.unpair e).1 = some a) : Encodable.encodeDecode ((a : α) × β a) e = Option.map (fun (b : ℕ) => Nat.pair (Encodable.encode a) b) (Encodable.encodeDecode (β a) (Nat.unpair e).2)

theorem Primcodable.ofEquiv_toEncodable {α : Type u_1} {β : Type u_2} [Primcodable α] (e : β ≃ α) : Primcodable.toEncodable = Encodable.ofEquiv α e

@[instance 100]

instance Primcodable.fintypeArrow {α : Type u_2} [DecidableEq α] [Fintype α] [Encodable α] (β : Type u_1) [Primcodable β] : Primcodable (α → β)

Equations

• Primcodable.fintypeArrow β = Primcodable.ofEquiv (Fin (Fintype.card α) → β) Encodable.fintypeArrowEquivFinArrow

theorem Primrec.decode_iff {α : Type u_1} {σ : Type u_6} [Primcodable α] [Primcodable σ] {f : α → σ} : (Primrec fun (n : ℕ) => Option.map f (Encodable.decode n)) ↔ Primrec f

theorem Primrec₂.decode_iff₁ {α : Type u_1} {β : Type u_4} {σ : Type u_6} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : (Primrec₂ fun (n : ℕ) (b : β) => Option.map (fun (x : α) => f x b) (Encodable.decode n)) ↔ Primrec₂ f

theorem Primrec₂.decode_iff₂ {α : Type u_1} {β : Type u_4} {σ : Type u_6} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} : (Primrec₂ fun (a : α) (n : ℕ) => Option.map (f a) (Encodable.decode n)) ↔ Primrec₂ f

theorem Primrec₂.of_equiv_iff {α : Type u_1} {σ : Type u_6} {τ : Type u_7} [Primcodable α] [Primcodable σ] [Primcodable τ] {β : Type u_8} (e : β ≃ α) {f : σ → τ → β} : (Primrec₂ fun (a : σ) (b : τ) => e (f a b)) ↔ Primrec₂ f

theorem Primrec.of_equiv_iff' {α : Type u_1} {σ : Type u_6} [Primcodable α] [Primcodable σ] {β : Type u_8} (e : β ≃ α) {f : β → σ} : (Primrec fun (b : α) => f (e.symm b)) ↔ Primrec f

theorem Primrec₂.of_equiv_iff'2 {α₁ : Type u_2} {α₂ : Type u_3} {σ : Type u_6} [Primcodable α₁] [Primcodable α₂] [Primcodable σ] {β : Type u_8} (e : β ≃ α₂) {f : α₁ → β → σ} : (Primrec₂ fun (a : α₁) (b : α₂) => f a (e.symm b)) ↔ Primrec₂ f

theorem Primrec.nat_strong_rec' {α : Type u_1} {σ : Type u_6} [Primcodable α] [Primcodable σ] (f : α → ℕ → σ) {g : α × ℕ → List σ → Option σ} (hg : Primrec₂ g) (H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)) : Primrec₂ f

theorem Primrec.nat_strong_rec'2 {α : Type u_1} {σ : Type u_6} [Primcodable α] [Primcodable σ] (f : α → ℕ × ℕ → σ) {g : α × ℕ × ℕ → List σ → Option σ} (hg : Primrec₂ g) (H : ∀ (a : α) (n m : ℕ), g (a, n, m) (List.map (fun (i : ℕ) => f a (Nat.unpair i)) (List.range (Nat.pair n m))) = some (f a (n, m))) : Primrec₂ f

theorem Primrec.nat_strong_rec'2' {σ : Type u_6} [Primcodable σ] (f : ℕ → ℕ → σ) {g : ℕ × ℕ → List σ → Option σ} (hg : Primrec₂ g) (H : ∀ (n m : ℕ), g (n, m) (List.map (fun (i : ℕ) => f (Nat.unpair i).1 (Nat.unpair i).2) (List.range (Nat.pair n m))) = some (f n m)) : Primrec₂ f

theorem Primrec.option_list_mapM' {α : Type u_1} {β : Type u_4} {γ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → List β} {g : α → β → Option γ} (hf : Primrec f) (hg : Primrec₂ g) : Primrec fun (a : α) => mapM' (g a) (f a)

theorem Primrec.to₂' {α : Type u_1} {β : Type u_4} {σ : Type u_6} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Primrec fun (p : α × β) => f p.1 p.2) : Primrec₂ f

theorem Primrec.of_list_decode_eq_some_cons {α : Type u_1} [Primcodable α] {a : α} {as : List α} {e : ℕ} : Encodable.decode e = some (a :: as) → Encodable.decode (Nat.unpair e.pred).1 = some a ∧ Encodable.decode (Nat.unpair e.pred).2 = some as

theorem Primrec.list_zipWith_param {α : Type u_1} {β : Type u_4} {γ : Type u_5} {σ : Type u_6} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : σ → α × β → γ} (hf : Primrec₂ f) : Primrec₂ fun (x : σ) (p : List α × List β) => List.zipWith (fun (a : α) (b : β) => f x (a, b)) p.1 p.2

theorem Primrec.list_zipWith {α : Type u_1} {β : Type u_4} {γ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → β → γ} (hf : Primrec₂ f) : Primrec₂ (List.zipWith f)

theorem Primrec.nat_predO : Primrec Nat.predO

theorem Primrec.encodeDecode {α : Type u_8} [Primcodable α] : Primrec fun (e : ℕ) => Encodable.encodeDecode α e

theorem Primrec.list_sup {α : Type u_8} [Primcodable α] [SemilatticeSup α] [OrderBot α] (hsup : Primrec₂ Sup.sup) : Primrec List.sup

theorem Primrec.option_get! {α : Type u_8} [Primcodable α] [Inhabited α] : Primrec Option.get!

class UniformlyPrimcodable {α : Type u} (β : α → Type v) [Primcodable α] [(a : α) → Primcodable (β a)] : Prop

• uniformly_prim : Primrec₂ fun (a : α) (n : ℕ) => Encodable.encode (Encodable.decode n)

theorem UniformlyPrimcodable.uniformly_prim {α : Type u} {β : α → Type v} [Primcodable α] [(a : α) → Primcodable (β a)] [self : UniformlyPrimcodable β] : Primrec₂ fun (a : α) (n : ℕ) => Encodable.encode (Encodable.decode n)

class PrimrecCard {α : Type u} (β : α → Type v) [(a : α) → Fintype (β a)] [Primcodable α] [(a : α) → Primcodable (β a)] : Prop

• card_prim : Primrec fun (a : α) => Fintype.card (β a)

theorem PrimrecCard.card_prim {α : Type u} {β : α → Type v} [(a : α) → Fintype (β a)] [Primcodable α] [(a : α) → Primcodable (β a)] [self : PrimrecCard β] : Primrec fun (a : α) => Fintype.card (β a)

theorem Primrec₂.encodeDecode_u {α : Type u} {β : α → Type v} [Primcodable α] [(a : α) → Primcodable (β a)] [UniformlyPrimcodable β] : Primrec₂ fun (a : α) (e : ℕ) => Encodable.encodeDecode (β a) e

def UniformlyPrimcodable.ofEncodeDecode {α : Type u} {β : α → Type v} [Primcodable α] [(a : α) → Primcodable (β a)] (h : Primrec₂ fun (a : α) (n : ℕ) => Encodable.encodeDecode (β a) n) : UniformlyPrimcodable β

Equations

• ⋯ = ⋯

def UniformlyPrimcodable.subtype {α : Type u} [Primcodable α] {β : Type u_1} [Primcodable β] {R : α → β → Prop} [(a : α) → (b : β) → Decidable (R a b)] (hR : PrimrecRel R) : UniformlyPrimcodable fun (a : α) => { x : β // R a x }

Equations

• ⋯ = ⋯

instance UniformlyPrimcodable.vector (β : Type u_1) [Primcodable β] : UniformlyPrimcodable (Mathlib.Vector β)

Equations

• ⋯ = ⋯

theorem UniformlyPrimcodable.qqqq {P : Prop} {Q : Prop} (h : P) (e : P = Q) : Q

instance UniformlyPrimcodable.finArrow (β : Type u_1) [Primcodable β] : UniformlyPrimcodable fun (x : ℕ) => Fin x → β

Equations

• ⋯ = ⋯

instance UniformlyPrimcodable.fintypeArrow {α : Type u} [Primcodable α] (γ : α → Type u_1) (β : Type u_2) [(a : α) → Fintype (γ a)] [(a : α) → DecidableEq (γ a)] [(a : α) → Primcodable (γ a)] [PrimrecCard γ] [Primcodable β] : UniformlyPrimcodable fun (x : α) => γ x → β

Equations

• ⋯ = ⋯

instance UniformlyPrimcodable.fin : UniformlyPrimcodable Fin

Equations

• UniformlyPrimcodable.fin = ⋯

instance UniformlyPrimcodable.prod {α : Type u} [Primcodable α] (β : α → Type u_1) (γ : α → Type u_2) [(a : α) → Primcodable (β a)] [(a : α) → Primcodable (γ a)] [UniformlyPrimcodable β] [UniformlyPrimcodable γ] : UniformlyPrimcodable fun (a : α) => β a × γ a

Equations

• ⋯ = ⋯

instance UniformlyPrimcodable.const {α : Type u} [Primcodable α] {β : Type u_1} [Primcodable β] : UniformlyPrimcodable fun (x : α) => β

Equations

• ⋯ = ⋯

instance Primcodable.sigma {α : Type u} {β : α → Type v} [Primcodable α] [(a : α) → Primcodable (β a)] [UniformlyPrimcodable β] : Primcodable (Sigma β)

Equations

• Primcodable.sigma = Primcodable.mk ⋯

@[simp]

theorem Primcodable.sigma_toEncodable_eq {α : Type u} {β : α → Type v} [Primcodable α] [(a : α) → Primcodable (β a)] [UniformlyPrimcodable β] : Primcodable.toEncodable = Sigma.encodable

@[irreducible]

theorem Encodable.decode_list {β : Type u_1} [Encodable β] (e : ℕ) : Encodable.decode e = mapM' Encodable.decode (Denumerable.ofNat (List ℕ) e)

theorem Encodable.decode_vector {β : Type u_1} [Encodable β] {k : ℕ} (e : ℕ) : Encodable.decode e = (Encodable.decode e).bind (List.toVector k)

theorem Encodable.decode_finArrow {k : ℕ} (β : Type u_2) [Primcodable β] (e : ℕ) : Encodable.decode e = (Encodable.decode e).bind fun (l : List β) => Option.map (⇑(Equiv.vectorEquivFin β k)) (List.toVector k l)

theorem Encodable.decode_fintypeArrow (ι : Type u_2) [Fintype ι] [Primcodable ι] [DecidableEq ι] (β : Type u_3) [Primcodable β] (e : ℕ) : Encodable.decode e = (Encodable.decode e).bind fun (l : List β) => Option.map (⇑Encodable.fintypeArrowEquivVector.symm) (List.toVector (Fintype.card ι) l)

theorem Encodable.encode_list {β : Type u_1} [Encodable β] (l : List β) : Encodable.encode l = Encodable.encode (List.map Encodable.encode l)

theorem Encodable.encode_vector {β : Type u_1} [Encodable β] {n : ℕ} (v : Mathlib.Vector β n) : Encodable.encode v = Encodable.encode v.toList

theorem Encodable.encode_finArrow {β : Type u_1} [Encodable β] {n : ℕ} (f : Fin n → β) : Encodable.encode f = Encodable.encode (List.ofFn f)

theorem Encodable.encode_finArrow' {β : Type u_1} [Encodable β] {k : ℕ} [Primcodable β] (f : Fin k → β) : Encodable.encode f = Encodable.encode fun (i : Fin k) => Encodable.encode (f i)

theorem Encodable.encode_fintypeArrow (ι : Type u_2) [Fintype ι] [Primcodable ι] [DecidableEq ι] (β : Type u_3) [Primcodable β] (f : ι → β) : Encodable.encode f = Encodable.encode (Encodable.fintypeArrowEquivFinArrow f)

theorem Encodable.encode_fintypeArrow' (ι : Type u_2) [Fintype ι] [Primcodable ι] [DecidableEq ι] (β : Type u_3) [Primcodable β] (f : ι → β) : Encodable.encode f = Encodable.encode fun (i : ι) => Encodable.encode (f i)

theorem Encodable.encode_fintypeArrow_isEmpty (ι : Type u_2) [Fintype ι] [Primcodable ι] [DecidableEq ι] [IsEmpty ι] (β : Type u_3) [Primcodable β] (f : ι → β) : Encodable.encode f = 0

theorem Encodable.encode_fintypeArrow_card_one {ι : Type u_2} [Fintype ι] [Primcodable ι] [DecidableEq ι] (hι : Fintype.card ι = 1) (β : Type u_3) [Primcodable β] (f : ι → β) (i : ι) : Encodable.encode f = Encodable.encode [f i]

theorem Encodable.encode_fintypeArrow_card_two {ι : Type u_2} [Fintype ι] [Primcodable ι] [DecidableEq ι] (hι : Fintype.card ι = 2) (β : Type u_3) [Primcodable β] (f : ι → β) : Encodable.encode f = Encodable.encode [f (Encodable.fintypeEquivFin.symm (Fin.cast ⋯ 0)), f (Encodable.fintypeEquivFin.symm (Fin.cast ⋯ 1))]

theorem Encodable.encode_list_lt {β : Type u_1} [Encodable β] {b : β} {bs : List β} (h : b ∈ bs) : Encodable.encode b < Encodable.encode bs

theorem Primrec.finArrow_list_ofFn {k : ℕ} {α : Type u_5} [Primcodable α] : Primrec List.ofFn

theorem Primrec.sigma_finArrow_list_ofFn {α : Type u_5} [Primcodable α] : Primrec fun (v : (k : ℕ) × (Fin k → α)) => List.ofFn v.snd

theorem Primrec.sigma_fst {α : Type u_2} {β : α → Type u_3} [Primcodable α] [(a : α) → Primcodable (β a)] [UniformlyPrimcodable β] : Primrec Sigma.fst

theorem Primrec.sigma_prod_left {α : Type u_7} {β : α → Type u_5} {γ : α → Type u_6} [Primcodable α] [(a : α) → Primcodable (β a)] [(a : α) → Primcodable (γ a)] [UniformlyPrimcodable β] [UniformlyPrimcodable γ] : Primrec fun (p : (a : α) × β a × γ a) => ⟨p.fst, p.snd.1⟩

theorem Primrec.sigma_prod_right {α : Type u_7} {β : α → Type u_5} {γ : α → Type u_6} [Primcodable α] [(a : α) → Primcodable (β a)] [(a : α) → Primcodable (γ a)] [UniformlyPrimcodable β] [UniformlyPrimcodable γ] : Primrec fun (p : (a : α) × β a × γ a) => ⟨p.fst, p.snd.2⟩

theorem Primrec.sigma_pair {α : Type u_2} {β : α → Type u_3} [Primcodable α] [(a : α) → Primcodable (β a)] [UniformlyPrimcodable β] (a : α) : Primrec (Sigma.mk a)

theorem Primrec.encode_of_uniform {α : Type u_2} {β : α → Type u_3} [Primcodable α] [(a : α) → Primcodable (β a)] {σ : Type u_5} [Primcodable σ] [UniformlyPrimcodable β] {b : σ → (a : α) × β a} (hb : Primrec b) : Primrec fun (x : σ) => Encodable.encode (b x).snd

theorem Primrec.finArrow_map {σ : Type u_1} {α : Type u_2} [Primcodable σ] [Primcodable α] {f : α → σ} (hf : Primrec f) (k : ℕ) : Primrec fun (v : Fin k → α) (i : Fin k) => f (v i)

theorem Primrec.finArrow_app {σ : Type u_1} {α : Type u_2} [Primcodable σ] [Primcodable α] {n : ℕ} {v : σ → Fin n → α} {f : σ → Fin n} (hv : Primrec v) (hf : Primrec f) : Primrec fun (x : σ) => v x (f x)

theorem Primrec.finite_change {α : Type u_2} [Primcodable α] {f : ℕ → α} (hf : Primrec f) (g : ℕ → α) (h : ∃ (m : ℕ), ∀ x ≥ m, g x = f x) : Primrec g

theorem Primrec.of_subtype_iff {α : Type u_2} [Primcodable α] {β : Type u_5} [Primcodable β] {p : α → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : β → { a : α // p a }} : (Primrec fun (x : β) => ↑(f x)) ↔ Primrec f

theorem Primrec₂.of_subtype_iff {α : Type u_2} [Primcodable α] {β : Type u_5} {γ : Type u_6} [Primcodable β] [Primcodable γ] {p : α → Prop} [DecidablePred p] {hp : PrimrecPred p} {f : β → γ → { a : α // p a }} : (Primrec₂ fun (x : β) (x_1 : γ) => ↑(f x x_1)) ↔ Primrec₂ f

theorem Primrec.nat_toFin {n : ℕ} : Primrec n.toFin

theorem Primrec.decide_eq_iff (p : Prop) [Decidable p] (b : Bool) : decide p = b ↔ (p ↔ b = true)

theorem Primrec.lawfulbeq {α : Type u_2} [Primcodable α] [BEq α] [LawfulBEq α] : Primrec₂ BEq.beq

theorem Primrec.list_mem {α : Type u_2} [Primcodable α] [BEq α] [LawfulBEq α] : PrimrecRel fun (x : α) (x_1 : List α) => x ∈ x_1

theorem Primrec.list_subset {α : Type u_2} [Primcodable α] [DecidableEq α] : PrimrecRel fun (x x_1 : List α) => x ⊆ x_1

theorem Primrec.list_all {α : Type u_5} {β : Type u_6} [Primcodable α] [Primcodable β] {p : α → β → Bool} {l : α → List β} (hp : Primrec₂ p) (hl : Primrec l) : Primrec fun (a : α) => (l a).all (p a)

theorem Primrec.list_replicate {α : Type u_5} [Primcodable α] : Primrec₂ List.replicate

theorem Computable.dom_bool {α : Type u_1} [Primcodable α] {f : Bool → α} : Computable f

theorem Computable.dom_bool₂ {α : Type u_1} [Primcodable α] {f : Bool → Bool → α} : Computable₂ f

theorem Computable₂.left {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Computable₂ fun (a : α) (x : β) => a

theorem Computable₂.right {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] : Computable₂ fun (x : α) (b : β) => b

theorem Computable.to₂' {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ} (hf : Computable fun (p : α × β) => f p.1 p.2) : Computable₂ f

theorem Computable.list_all {α : Type u_4} {β : Type u_5} [Primcodable α] [Primcodable β] {p : α → β → Bool} {l : α → List β} (hp : Computable₂ p) (hl : Computable l) : Computable fun (a : α) => (l a).all (p a)

noncomputable def PFun.merge {α : Type u_1} {σ : Type u_3} (f : α →. σ) (g : α →. σ) : α →. σ

Equations

• f.merge g = Classical.epsilon fun (k : α →. σ) => ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a

theorem Partrec.merge_iff {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α →. σ} (hf : Partrec f) (hg : Partrec g) (H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y) {a : α} {x : σ} : x ∈ f.merge g a ↔ x ∈ f a ∨ x ∈ g a

theorem Partrec.mergep {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α →. σ} (hf : Partrec f) (hg : Partrec g) (H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y) : Partrec (f.merge g)