case intro.intro
α : Type u_1
σ : Type ?u.282635
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ ComputablePred fun a => f a = true
α : Type u_1
σ : Type ?u.282635
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
p : α → Prop
⊢ (∃ f, Computable f ∧ p = fun a => f a = true) → ComputablePred p
rintro ⟨f, h, rfl⟩
no goals
case intro.intro
α : Type u_1
σ : Type ?u.282635
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ ComputablePred fun a => f a = true
exact ⟨by infer_instance, by simpa using h⟩
no goals
α : Type u_1
σ : Type ?u.282635
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ DecidablePred fun a => f a = true
infer_instance
no goals
α : Type u_1
σ : Type ?u.282635
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → Bool
h : Computable f
⊢ Computable fun a => decide ((fun a => f a = true) a)
simpa using h