Skip to content

[ deprecate ] README.Inspect #2928

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

Open
jamesmckinna wants to merge 3 commits into
base: master
Choose a base branch
from
Open

[ deprecate ] README.Inspect #2928

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
49dcb48
remove: `import README.Inspect`
jamesmckinna Feb 4, 2026
7a07c22
deprecate: `README.Inspect`
jamesmckinna Feb 4, 2026
86e5eb8
add: forward pointer to the v2.9.0 docs
jamesmckinna Feb 6, 2026
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
5 changes: 0 additions & 5 deletions doc/README.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,11 +241,6 @@ import README.Debug.Trace

import README.Nary

-- Explaining the inspect idiom: use case, equivalent handwritten
-- auxiliary definitions, and implementation details.

import README.Inspect

-- Explaining how to use the automatic solvers

import README.Tactic.MonoidSolver
Expand Down
13 changes: 11 additions & 2 deletions doc/README/Inspect.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,23 @@
------------------------------------------------------------------------
-- The Agda standard library
--
-- Explaining how to use the inspect idiom and elaborating on the way
-- it is implemented in the standard library.
-- This module is DEPRECATED.
Copy link
Copy Markdown
Collaborator

@MatthewDaggitt MatthewDaggitt Feb 6, 2026

Choose a reason for hiding this comment

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

Could we add a pointer towards the Agda documentation on the with idiom instead?

Copy link
Copy Markdown
Collaborator Author

@jamesmckinna jamesmckinna Feb 6, 2026 •
edited
Loading

Choose a reason for hiding this comment

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

Yes. I'd been going to add that, as previously, to the deprecation section of Relation.Binary.PropositionalEquality.Core, but happy to do so here too.

But NB. the upstream change will only arise in v2.9.0, but AFAIK, there aren't readthedocs pages for that release... yet... so there's a more annoying synchronisation problem, by contrast with #2931 / #2932

UPDATED: latest commit makes a forward-in-time pointer to the v2.9.0, assuming we sort out a sensible v2.4 release schedule for which this makes sense...

Copy link
Copy Markdown
Collaborator Author

@jamesmckinna jamesmckinna Feb 6, 2026

Choose a reason for hiding this comment

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

Going back over #1930, I realised that I'd failed to push the claimed README.WithIn to explain the new syntax, on the model of the previous README.Inspect.

One thing to do might be to reinstate it as part of this PR, but I'd need to find it, and work out if it still makes sense against the new semantics!

Let me know whether you think this worthwhile before I push look for, never mind push, anything else!

--
-- The record type `Reveal_·_is_`, and its principal mode of use,
-- via the `inspect` function described below, have been deprecated
-- in favour of the `with ... in ...` syntax. See the documentation
--
-- https://agda.readthedocs.io/en/v2.9.0/language/with-abstraction.html#with-abstraction-equality
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module README.Inspect where

{-# WARNING_ON_IMPORT
"README.Inspect was deprecated in v2.4."
#-}

open import Data.Nat.Base
open import Data.Nat.Properties
open import Data.Product.Base using (_×_; _,_)
Expand Down
Loading