[fixes #2127] Fixes #1930 import bug (#2128)

Author: jamesmckinna

README.agda

@@ -237,6 +237,11 @@ 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

README/Inspect.agda

@@ -1,22 +1,19 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- This module is DEPRECATED.
+-- Explaining how to use the inspect idiom and elaborating on the way
+-- it is implemented in the standard library.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 module README.Inspect where
 
-{-# WARNING_ON_IMPORT
-"README.Inspect was deprecated in v2.0."
-#-}
-
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product.Base using (_×_; _,_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Binary.PropositionalEquality using (inspect)
+open import Relation.Binary.PropositionalEquality using (inspect; [_])
 
 ------------------------------------------------------------------------
 -- Using inspect