------------------------------------------------------------------------ -- The Agda standard library -- -- Some properties imply others ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Relation.Unary.Consequences where open import Relation.Unary open import Relation.Nullary using (recompute) dec⟶recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P dec⟶recomputable P-dec = recompute (P-dec _)