no goals
α : Type u_1
σ : Type ?u.313648
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
⊢ ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a
classical exact computable_iff_re_compl_re
no goals
α : Type u_1
σ : Type ?u.313648
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
⊢ ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a
exact computable_iff_re_compl_re