From 7fbffe1ce0b610ef9e281e4fa02357708a4074a7 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 27 Sep 2023 12:08:18 +0900 Subject: [PATCH] Undeprecate inspect idiom --- CHANGELOG.md | 10 +------- .../Binary/PropositionalEquality.agda | 23 +++++++------------ 2 files changed, 9 insertions(+), 24 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5a42872be0..6289aae108 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1547,14 +1547,6 @@ Deprecated names * This fixes the fact we had picked the wrong name originally. The erased modality corresponds to @0 whereas the irrelevance one corresponds to `.`. -### Deprecated `Relation.Binary.PropositionalEquality.inspect` - in favour of `with ... in ...` syntax (issue #1580; PRs #1630, #1930) - -* In `Relation.Binary.PropositionalEquality` - both the record type `Reveal_·_is_` - and its principal mode of use, `inspect`, - have been deprecated in favour of the new `with ... in ...` syntax. - See the documentation of [with-abstraction equality](https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality) New modules ----------- @@ -3484,4 +3476,4 @@ This is a full list of proofs that have changed form to use irrelevant instance b #⟨ b#c ⟩ c ≈⟨ c≈d ⟩ d ∎ - ``` \ No newline at end of file + ``` diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 418e9b2ade..6ff59d8c28 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -104,15 +104,17 @@ module _ (_≟_ : DecidableEquality A) {x y : A} where ≢-≟-identity = dec-no (x ≟ y) +------------------------------------------------------------------------ +-- Inspect +-- Inspect can be used when you want to pattern match on the result r +-- of some expression e, and you also need to "remember" that r ≡ e. ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. +-- See README.Inspect for an explanation of how/why to use this. --- Version 2.0 +-- Normally (but not always) the new `with ... in` syntax described at +-- https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality +-- can be used instead." record Reveal_·_is_ {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) (y : B x) : @@ -123,12 +125,3 @@ record Reveal_·_is_ {A : Set a} {B : A → Set b} inspect : ∀ {A : Set a} {B : A → Set b} (f : (x : A) → B x) (x : A) → Reveal f · x is f x inspect f x = [ refl ] - -{-# WARNING_ON_USAGE Reveal_·_is_ -"Warning: Reveal_·_is_ was deprecated in v2.0. -Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead." -#-} -{-# WARNING_ON_USAGE inspect -"Warning: inspect was deprecated in v2.0. -Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.3/language/with-abstraction.html#with-abstraction-equality instead." -#-}