Skip to content

Un-deprecate inspect idiom #2107

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MatthewDaggitt merged 1 commit into from
Sep 27, 2023
Merged

Un-deprecate inspect idiom #2107

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 1 addition & 9 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
-----------
Expand Down Expand Up @@ -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 ∎
```
```
23 changes: 8 additions & 15 deletions src/Relation/Binary/PropositionalEquality.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Collaborator

@jamesmckinna jamesmckinna Sep 27, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

'result' or 'value'?
(I realise this is the previous text, but I wonder if this is more precise usage?)

-- of some expression e, and you also need to "remember" that r ≡ e.
Copy link
Collaborator

@jamesmckinna jamesmckinna Sep 27, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One of the (many? subtle!) peculiarities of inspect us that it does rely of e being of the form f a and requires you to identify those pieces separately. That is, there seems no way to fold together with e with an invocation of inspect e (the latter makes no sense per se) in a single statement form.

Unless one perhaps writes directly

with inspect {.(f a)} f a
... | eq = ...

but even then the explicit dot-patterned term is not bound to a(n independent) variable subsequently available to the matcher.

So even the pragmatic of this notation are both annoying, and hard to explain well...


------------------------------------------------------------------------
-- 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) :
Expand All @@ -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."
#-}