α : Type u_1
β : Type ?u.353649
γ : Type ?u.353652
σ : Type ?u.353655
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ Primrec Subtype.val
α : Type u_1
β : Type ?u.353649
γ : Type ?u.353652
σ : Type ?u.353655
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
⊢ Primrec Subtype.val
letI := Primcodable.subtype hp
α : Type u_1
β : Type ?u.353649
γ : Type ?u.353652
σ : Type ?u.353655
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode (decode n) = encode (Option.map Subtype.val (decode n))
α : Type u_1
β : Type ?u.353649
γ : Type ?u.353652
σ : Type ?u.353655
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
⊢ Primrec Subtype.val
refine' (@Primcodable.prim (Subtype p)).of_eq fun n => _
no goals
α : Type u_1
β : Type ?u.353649
γ : Type ?u.353652
σ : Type ?u.353655
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
p : α → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
this : Primcodable (Subtype p) := Primcodable.subtype hp
n : ℕ
⊢ encode (decode n) = encode (Option.map Subtype.val (decode n))
rcases @decode (Subtype p) _ n with (_ | ⟨a, h⟩) <;> rfl