From 49dcb48f7640a36423f4a41f2dd4443db39577a5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Feb 2026 09:08:37 +0000 Subject: [PATCH 1/3] remove: `import README.Inspect` --- doc/README.agda | 5 ----- 1 file changed, 5 deletions(-) diff --git a/doc/README.agda b/doc/README.agda index b1c969fd71..f17fb75eb7 100644 --- a/doc/README.agda +++ b/doc/README.agda @@ -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 From 7a07c22e681692362e98cb0de50f3ff5a6159d8d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Feb 2026 09:09:10 +0000 Subject: [PATCH 2/3] deprecate: `README.Inspect` --- doc/README/Inspect.agda | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/doc/README/Inspect.agda b/doc/README/Inspect.agda index 2199a499c8..4b9045e956 100644 --- a/doc/README/Inspect.agda +++ b/doc/README/Inspect.agda @@ -1,14 +1,17 @@ ------------------------------------------------------------------------ -- 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. ------------------------------------------------------------------------ {-# 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 (_×_; _,_) From 86e5eb818c26e2120769c6b512b552756f448efb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 6 Feb 2026 09:31:09 +0000 Subject: [PATCH 3/3] add: forward pointer to the v2.9.0 docs --- doc/README/Inspect.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/README/Inspect.agda b/doc/README/Inspect.agda index 4b9045e956..406e47e56b 100644 --- a/doc/README/Inspect.agda +++ b/doc/README/Inspect.agda @@ -2,6 +2,12 @@ -- The Agda standard library -- -- This module is DEPRECATED. +-- +-- 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 #-}