diff --git a/CHANGELOG.md b/CHANGELOG.md index a1fb08efcf..b321485c05 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1776,6 +1776,11 @@ Deprecated names map-++-commute ↦ map-++ ``` +* In `Function.Base`: + ``` + case_return_of_ ↦ case_returning_of_ + ``` + * In `Function.Construct.Composition`: ``` _∘-⟶_ ↦ _⟶-∘_ diff --git a/README/Case.agda b/README/Case.agda index 30ce0221aa..62fec18c0f 100644 --- a/README/Case.agda +++ b/README/Case.agda @@ -12,7 +12,7 @@ module README.Case where open import Data.Fin hiding (pred) open import Data.Maybe hiding (from-just) open import Data.Nat hiding (pred) -open import Function.Base using (case_of_; case_return_of_) +open import Function.Base using (case_of_; case_returning_of_) open import Relation.Nullary ------------------------------------------------------------------------ @@ -35,7 +35,7 @@ pred n = case n of λ -- where-introduced and indentation-identified block of list of clauses from-just : ∀ {a} {A : Set a} (x : Maybe A) → From-just x -from-just x = case x return From-just of λ where +from-just x = case x returning From-just of λ where (just x) → x nothing → _ diff --git a/src/Function/Base.agda b/src/Function/Base.agda index 9bdb996dc8..122e276469 100644 --- a/src/Function/Base.agda +++ b/src/Function/Base.agda @@ -110,10 +110,10 @@ f $- = f _ -- Case expressions (to be used with pattern-matching lambdas, see -- README.Case). -case_return_of_ : ∀ {A : Set a} (x : A) (B : A → Set b) → +case_returning_of_ : ∀ {A : Set a} (x : A) (B : A → Set b) → ((x : A) → B x) → B x -case x return B of f = f x -{-# INLINE case_return_of_ #-} +case x returning B of f = f x +{-# INLINE case_returning_of_ #-} ------------------------------------------------------------------------ -- Non-dependent versions of dependent operations @@ -156,7 +156,7 @@ _|>′_ = _|>_ -- README.Case). case_of_ : A → (A → B) → B -case x of f = case x return _ of f +case x of f = case x returning _ of f {-# INLINE case_of_ #-} ------------------------------------------------------------------------ @@ -247,10 +247,24 @@ _*_ on f = f -⟨ _*_ ⟩- f ------------------------------------------------------------------------ --- Deprecated +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 1.4 _-[_]-_ = _-⟪_⟫-_ {-# WARNING_ON_USAGE _-[_]-_ "Warning: Function._-[_]-_ was deprecated in v1.4. Please use _-⟪_⟫-_ instead." #-} + +-- Version 2.0 + +case_return_of_ = case_returning_of_ +{-# WARNING_ON_USAGE case_return_of_ +"case_return_of_ was deprecated in v2.0. +Please use case_returning_of_ instead." +#-} +