------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties imply others
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Unary.Consequences where
open import Relation.Unary using (Pred; Recomputable; Decidable)
open import Relation.Nullary.Decidable.Core using (recompute)
dec⇒recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
dec⇒recomputable P-dec = recompute (P-dec _)
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
dec⟶recomputable = dec⇒recomputable
{-# WARNING_ON_USAGE dec⟶recomputable
"Warning: dec⟶recomputable was deprecated in v2.0.
Please use dec⇒recomputable instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4