def WType.inversion {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] : WType β → α × List (WType β)

Equations

• x.inversion = match x with | WType.mk a f => (a, List.ofFn (Encodable.fintypeArrowEquivFinArrow f))

def WType.elimv {α : Type u_1} {β : α → Type u_2} {σ : Type u_3} {γ : Type u_4} (fs : α → σ → σ) (fγ : σ → (a : α) × (β a → γ) → γ) : σ → WType β → γ

Equations

• WType.elimv fs fγ x (WType.mk a f) = fγ x ⟨a, fun (b : β a) => WType.elimv fs fγ (fs a x) (f b)⟩

def WType.elimOpt {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (γ : Type u_3) (fγ : (a : α) × (β a → γ) → Option γ) : WType β → Option γ

Equations

• WType.elimOpt γ fγ (WType.mk a f) = (Encodable.toFinArrowOpt fun (b : β a) => WType.elimOpt γ fγ (f b)).bind fun (g : β a → γ) => fγ ⟨a, g⟩

def WType.SubWType {α : Type u_3} (β : α → Type u_4) [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (n : ℕ) : Type (max 0 u_3 u_4)

Equations

• WType.SubWType β n = { t : WType β // t.depth ≤ n }

theorem WType.SubWType.ext {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s : ℕ} (w₁ : WType.SubWType β s) (w₂ : WType.SubWType β s) : ↑w₁ = ↑w₂ → w₁ = w₂

def WType.SubWType.cast {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s : ℕ} {s' : ℕ} (hs : s = s') (w : WType.SubWType β s) : WType.SubWType β s'

Equations

• WType.SubWType.cast hs w = ⟨↑w, ⋯⟩

@[simp]

def WType.SubWType.cast_refl {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s : ℕ} (h : s = s) (w : WType.SubWType β s) : WType.SubWType.cast h w = w

Equations

• ⋯ = ⋯

def WType.SubWType.mk {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s : ℕ} (a : α) (f : β a → WType.SubWType β s) : WType.SubWType β (s + 1)

Equations

• WType.SubWType.mk a f = ⟨WType.mk a fun (i : β a) => ↑(f i), ⋯⟩

@[simp]

theorem WType.SubWType.cast_mk {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s : ℕ} {s' : ℕ} (hs : s + 1 = s' + 1) (a : α) (f : β a → WType.SubWType β s) : WType.SubWType.cast hs (WType.SubWType.mk a f) = WType.SubWType.mk a fun (i : β a) => WType.SubWType.cast ⋯ (f i)

@[simp]

theorem WType.SubWType.cast_mk_one {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s : ℕ} (hs : s + 1 = 1) (a : α) (f : β a → WType.SubWType β s) : WType.SubWType.cast hs (WType.SubWType.mk a f) = WType.SubWType.mk a fun (i : β a) => WType.SubWType.cast ⋯ (f i)

@[reducible, inline]

abbrev WType.SubWType.ofWType {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (w : WType β) (n : ℕ) (h : w.depth ≤ n) : WType.SubWType β n

Equations

• WType.SubWType.ofWType w n h = ⟨w, h⟩

@[simp]

theorem WType.SubWType.depth_le {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {n : ℕ} (t : WType.SubWType β n) : (↑t).depth ≤ n

@[reducible, inline]

abbrev WType.SubWType.elim' {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (γ : Type u_3) (fγ : (a : α) × (β a → γ) → γ) (s : ℕ) : WType.SubWType β s → γ

Equations

• WType.SubWType.elim' γ fγ s x = match x with | ⟨t, property⟩ => WType.elim γ fγ t

theorem WType.SubWType.elim_const {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {s₁ : ℕ} {s₂ : ℕ} {w₁ : WType.SubWType β s₁} {w₂ : WType.SubWType β s₂} (h : ↑w₁ = ↑w₂) (γ : Type u_3) (fγ : (a : α) × (β a → γ) → γ) : WType.SubWType.elim' γ fγ s₁ w₁ = WType.SubWType.elim' γ fγ s₂ w₂

def WType.SubWType.equiv_zero {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] : WType.SubWType β 0 ≃ Empty

Equations

• One or more equations did not get rendered due to their size.

def WType.SubWType.equiv_succ {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {n : ℕ} : WType.SubWType β (n + 1) ≃ (a : α) × (β a → WType.SubWType β n)

Equations

• One or more equations did not get rendered due to their size.

def WType.SubWType.primcodable_zero {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] : Primcodable (WType.SubWType β 0)

Equations

• WType.SubWType.primcodable_zero = Primcodable.ofEquiv Empty WType.SubWType.equiv_zero

def WType.SubWType.primcodable_succ {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (n : ℕ) : Primcodable (WType.SubWType β n) → Primcodable (WType.SubWType β (n + 1))

Equations

• WType.SubWType.primcodable_succ n x = Primcodable.ofEquiv ((a : α) × (β a → WType.SubWType β n)) WType.SubWType.equiv_succ

instance Primcodable.SubWType {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (n : ℕ) : Primcodable (WType.SubWType β n)

Equations

• Primcodable.SubWType n = Nat.rec WType.SubWType.primcodable_zero WType.SubWType.primcodable_succ n

@[simp]

theorem WType.SubWType.decode_zero {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {e : ℕ} : Encodable.decode e = none

theorem WType.SubWType.decode_succ {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {s : ℕ} {e : ℕ} : Encodable.decode e = (Encodable.decode (Nat.unpair e).1).bind fun (a : α) => (Encodable.decode (Nat.unpair e).2).bind fun (l : List (WType.SubWType β s)) => Option.map (fun (v : Mathlib.Vector (WType.SubWType β s) (Fintype.card (β a))) => WType.SubWType.ofWType (WType.mk a fun (b : β a) => ↑(Encodable.fintypeArrowEquivVector.symm v b)) (s + 1) ⋯) (List.toVector (Fintype.card (β a)) l)

theorem WType.SubWType.encode_mk {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {s : ℕ} (a : α) (f : β a → WType β) (h : (WType.mk a f).depth ≤ s + 1) : Encodable.encode (WType.SubWType.ofWType (WType.mk a f) (s + 1) h) = Nat.pair (Encodable.encode a) (Encodable.encode fun (b : β a) => Encodable.encode (WType.SubWType.ofWType (f b) s ⋯))

theorem WType.SubWType.encode_cast {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {s : ℕ} (w : WType.SubWType β s) {s' : ℕ} (hs : s = s') : Encodable.encode w = Encodable.encode (WType.SubWType.cast hs w)

def WType.SubWType.elimDecode {α : Type u_1} (β : α → Type u_2) [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {γ : Type u_4} (f : α → List γ → γ) : ℕ → ℕ → Option γ

Equations

• One or more equations did not get rendered due to their size.

theorem WType.SubWType.elimDecode_eq_induction {α : Type u_1} (β : α → Type u_2) [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {γ : Type u_4} (f : α → List γ → γ) (s : ℕ) (e : ℕ) : WType.SubWType.elimDecode β f s e = Nat.casesOn s none fun (s : ℕ) => (Encodable.decode (Nat.unpair e).1).bind fun (a : α) => Option.map (fun (v : List γ) => f a v) ((mapM' (WType.SubWType.elimDecode β f s) (Denumerable.ofNat (List ℕ) (Nat.unpair e).2)).bind fun (l : List γ) => if l.length = Fintype.card (β a) then some l else none)

theorem WType.SubWType.primrec_elimDecode_param {α : Type u_1} (β : α → Type u_2) [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {σ : Type u_3} {γ : Type u_4} [Primcodable σ] [Primcodable γ] {f : σ → α × List γ → γ} (hf : Primrec₂ f) : Primrec₂ fun (x : σ) (p : ℕ × ℕ) => WType.SubWType.elimDecode β (fun (a : α) (ih : List γ) => f x (a, ih)) p.1 p.2

theorem WType.SubWType.primrec_elimDecode {α : Type u_1} (β : α → Type u_2) [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {γ : Type u_4} [Primcodable γ] {f : α → List γ → γ} (hf : Primrec₂ f) : Primrec₂ fun (s e : ℕ) => WType.SubWType.elimDecode β f s e

theorem WType.SubWType.primrec_elimDecode_param_comp {α : Type u_1} (β : α → Type u_2) [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {σ : Type u_3} {γ : Type u_4} [Primcodable σ] [Primcodable γ] {f : σ → α × List γ → γ} {g : σ → ℕ} {h : σ → ℕ} (hf : Primrec₂ f) (hg : Primrec g) (hh : Primrec h) : Primrec fun (x : σ) => WType.SubWType.elimDecode β (fun (a : α) (l : List γ) => f x (a, l)) (g x) (h x)

theorem WType.SubWType.encode_eq_elim' {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {s : ℕ} (w : WType.SubWType β s) : Encodable.encode w = WType.SubWType.elim' ℕ Encodable.encode s w

theorem WType.SubWType.encodeDecode_eq_elimDecode {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (s : ℕ) (e : ℕ) : Encodable.encodeDecode (WType.SubWType β s) e = WType.SubWType.elimDecode β (fun (a : α) (l : List ℕ) => Encodable.encode (a, l)) s e

instance WType.SubWType.uniformlyPrimcodable {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] : UniformlyPrimcodable (WType.SubWType β)

Equations

• ⋯ = ⋯

theorem WType.SubWType.depth_eq_elimDecode {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (s : ℕ) (e : ℕ) : Option.map (fun (w : WType.SubWType β s) => (↑w).depth) (Encodable.decode e) = WType.SubWType.elimDecode β (fun (a : α) (l : List ℕ) => l.sup + 1) s e

theorem WType.SubWType.depth_decode_primrec {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] : Primrec₂ fun (s e : ℕ) => Option.map (fun (w : WType.SubWType β s) => (↑w).depth) (Encodable.decode e)

def WType.SubWType.ofW {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] : WType β → (s : ℕ) × WType.SubWType β s

Equations

• WType.SubWType.ofW w = ⟨w.depth, WType.SubWType.ofWType w w.depth ⋯⟩

def WType.SubWType.toW {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] : (s : ℕ) × WType.SubWType β s → WType β

Equations

• WType.SubWType.toW x = match x with | ⟨fst, w⟩ => ↑w

def Encodable.wtype {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] : Encodable (WType β)

Equations

• Encodable.wtype = { encode := fun (w : WType β) => Encodable.encode (WType.SubWType.ofW w), decode := fun (e : ℕ) => Option.map WType.SubWType.toW (Encodable.decode e), encodek := ⋯ }

instance Primcodable.wtype {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] : Primcodable (WType β)

Equations

• Primcodable.wtype = let __src := Encodable.wtype; Primcodable.mk ⋯

theorem WType.encode_eq {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (w : WType β) : Encodable.encode w = Encodable.encode (WType.SubWType.ofW w)

theorem WType.decode_eq {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (e : ℕ) : Encodable.decode e = Option.map WType.SubWType.toW (Encodable.decode e)

def WType.elimL {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {γ : Type u_3} (f : α → List γ → γ) : WType β → γ

Equations

• WType.elimL f = WType.elim γ fun (x : (a : α) × (β a → γ)) => match x with | ⟨a, v⟩ => f a (List.ofFn (Encodable.fintypeArrowEquivFinArrow v))

theorem WType.elimL_mk {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {γ : Type u_3} (f : α → List γ → γ) (a : α) (v : β a → WType β) : WType.elimL f (WType.mk a v) = f a (List.ofFn (Encodable.fintypeArrowEquivFinArrow fun (b : β a) => WType.elimL f (v b)))

theorem WType.elim_eq_elimL {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {γ : Type u_3} {w : WType β} [Inhabited γ] (f : (a : α) × (β a → γ) → γ) : WType.elim γ f w = WType.elimL (fun (a : α) (l : List γ) => f ⟨a, Encodable.fintypeArrowEquivFinArrow.symm fun (i : Fin (Fintype.card (β a))) => l.getI ↑i⟩) w

theorem WType.decode_elimL_eq {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] {γ : Type u_3} {e : ℕ} (f : α → List γ → γ) : Option.map (WType.elimL f) (Encodable.decode e) = WType.SubWType.elimDecode β f (Nat.unpair e).1 (Nat.unpair e).2

def WType.elimvL {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {σ : Type u_3} {γ : Type u_4} (fs : α → σ → σ) (fγ : σ → α → List γ → γ) : σ → WType β → γ

Equations

• WType.elimvL fs fγ = WType.elimv fs fun (x : σ) (x_1 : (a : α) × (β a → γ)) => match x_1 with | ⟨a, v⟩ => fγ x a (List.ofFn (Encodable.fintypeArrowEquivFinArrow v))

theorem WType.elimvL_mk {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {σ : Type u_3} {γ : Type u_4} {x : σ} (fs : α → σ → σ) (fγ : σ → α → List γ → γ) (a : α) (v : β a → WType β) : WType.elimvL fs fγ x (WType.mk a v) = fγ x a (List.ofFn (Encodable.fintypeArrowEquivFinArrow fun (b : β a) => WType.elimvL fs fγ (fs a x) (v b)))

def WType.mkL {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (a : α) (l : List (WType β)) : Option (WType β)

Equations

• One or more equations did not get rendered due to their size.

def WType.mkFintype {α : Type u_1} {β : α → Type u_2} (a : α) (v : β a → WType β) : WType β

Equations

• WType.mkFintype a v = WType.mk a v

def WType.mk₀ {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (a : α) : Option (WType β)

Equations

• WType.mk₀ a = WType.mkL a []

def WType.mk₁ {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (a : α) (w : WType β) : Option (WType β)

Equations

• WType.mk₁ a w = WType.mkL a [w]

def WType.mkFin {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] {k : ℕ} (a : α) (v : Fin k → WType β) : Option (WType β)

Equations

• WType.mkFin a v = WType.mkL a (List.ofFn v)

theorem WType.encode_mk_eq {α : Type u_1} {β : α → Type u_2} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (a : α) (f : β a → WType β) : Encodable.encode (WType.mk a f) = Nat.pair ((Finset.univ.sup fun (n : β a) => (f n).depth) + 1) (Nat.pair (Encodable.encode a) (Encodable.encode fun (b : β a) => (Nat.unpair (Encodable.encode (f b))).2))

theorem WType.mk₀_eq {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (a : α) [h : IsEmpty (β a)] : WType.mk₀ a = some (WType.mk a h.elim')

theorem WType.mkL_inversion {α : Type u_1} {β : α → Type u_2} [(a : α) → Fintype (β a)] [(a : α) → Primcodable (β a)] (w : WType β) : WType.mkL w.inversion.1 w.inversion.2 = some w

theorem Primrec.w_depth {α : Type u_3} {β : α → Type u_5} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] : Primrec WType.depth

theorem Primrec.w_elimL {α : Type u_3} {γ : Type u_4} {β : α → Type u_5} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] [Primcodable γ] {f : α → List γ → γ} (hf : Primrec₂ f) : Primrec (WType.elimL f)

theorem Primrec.w_elimL_param {σ : Type u_2} {α : Type u_3} {γ : Type u_4} {β : α → Type u_5} [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] [Primcodable γ] {f : σ → α × List γ → γ} {w : σ → WType β} (hf : Primrec₂ f) (hw : Primrec w) : Primrec fun (x : σ) => WType.elimL (fun (p : α) (l : List γ) => f x (p, l)) (w x)

theorem Primrec.w_elim {α : Type u_3} {γ : Type u_4} {β : α → Type u_5} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] [Primcodable γ] [Inhabited γ] {f : (a : α) × (β a → γ) → γ} (hf : Primrec₂ fun (a : α) (l : List γ) => f ⟨a, Encodable.fintypeArrowEquivFinArrow.symm fun (i : Fin (Fintype.card (β a))) => l.getI ↑i⟩) : Primrec (WType.elim γ f)

theorem Primrec.w_mkL {α : Type u_3} {β : α → Type u_5} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] : Primrec₂ WType.mkL

theorem Primrec.w_mk₀ {σ : Type u_2} {α : Type u_3} {β : α → Type u_5} [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (f : σ → α) (h : ∀ (x : σ), IsEmpty (β (f x))) (hf : Primrec f) {v : {x : σ} → β (f x) → WType β} : Primrec fun (x : σ) => WType.mk (f x) v

theorem Primrec.w_mk₁ {σ : Type u_2} {α : Type u_3} {β : α → Type u_5} [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (f : σ → α) (h : ∀ (x : σ), Fintype.card (β (f x)) = 1) (hf : Primrec f) : Primrec₂ fun (x : σ) (w : WType β) => WType.mk (f x) fun (x : β (f x)) => w

theorem Primrec.w_mk₂ {σ : Type u_2} {α : Type u_3} {β : α → Type u_5} [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (f : σ → α) (h : ∀ (x : σ), Fintype.card (β (f x)) = 2) (hf : Primrec f) : Primrec₂ fun (x : σ) (w : WType β × WType β) => WType.mk (f x) ((Encodable.fintypeArrowEquivFinArrow' ⋯).symm ![w.1, w.2])

theorem Primrec.w_mkFin {σ : Type u_2} {α : Type u_3} {β : α → Type u_5} [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] (f : σ → α) {k : ℕ} (h : ∀ (x : σ), Fintype.card (β (f x)) = k) (hf : Primrec f) : Primrec₂ fun (x : σ) (w : Fin k → WType β) => WType.mk (f x) ((Encodable.fintypeArrowEquivFinArrow' ⋯).symm w)

theorem Primrec.w_inversion {α : Type u_3} {β : α → Type u_5} [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] [Inhabited (WType β)] : Primrec WType.inversion

theorem Primrec.w_elimvL_param {τ : Type u_1} {σ : Type u_2} {α : Type u_3} {γ : Type u_4} {β : α → Type u_5} [Primcodable τ] [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] [Primcodable γ] [Inhabited (WType β)] {fs : τ → α × σ → σ} {fγ : τ → σ × α × List γ → γ} {g : τ → σ} {w : τ → WType β} (hfs : Primrec₂ fs) (hfγ : Primrec₂ fγ) (hg : Primrec g) (hw : Primrec w) : Primrec fun (z : τ) => WType.elimvL (fun (a : α) (x : σ) => fs z (a, x)) (fun (x : σ) (a : α) (l : List γ) => fγ z (x, a, l)) (g z) (w z)

theorem Primrec.w_elimvL {σ : Type u_2} {α : Type u_3} {γ : Type u_4} {β : α → Type u_5} [Primcodable σ] [Primcodable α] [(a : α) → Fintype (β a)] [(a : α) → DecidableEq (β a)] [(a : α) → Primcodable (β a)] [PrimrecCard β] [Primcodable γ] [Inhabited (WType β)] {fs : α → σ → σ} {fγ : σ → α × List γ → γ} (hfs : Primrec₂ fs) (hfγ : Primrec₂ fγ) : Primrec₂ (WType.elimvL fs fun (x : σ) (a : α) (l : List γ) => fγ x (a, l))