From 1b13835c9c209a49520325ed78c67ca812ff0153 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 9 Oct 2023 11:44:55 +0100 Subject: [PATCH 1/3] fixed #1930 bug --- README/Inspect.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README/Inspect.agda b/README/Inspect.agda index 9f40a8d65a..b76eec729f 100644 --- a/README/Inspect.agda +++ b/README/Inspect.agda @@ -16,7 +16,7 @@ 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 From a76e335f7d0343151d3c5c3e2b8aa3ef0ba26d03 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 9 Oct 2023 12:09:59 +0100 Subject: [PATCH 2/3] undeprecated `README.Inspect` --- README/Inspect.agda | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/README/Inspect.agda b/README/Inspect.agda index b76eec729f..2199a499c8 100644 --- a/README/Inspect.agda +++ b/README/Inspect.agda @@ -1,17 +1,14 @@ ------------------------------------------------------------------------ -- 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 (_×_; _,_) From e920854ffd48e31222f35376e49d6d01b2c79225 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 9 Oct 2023 12:10:47 +0100 Subject: [PATCH 3/3] restored `README.Inspect` --- README.agda | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.agda b/README.agda index 97b8ab3903..ced0f11596 100644 --- a/README.agda +++ b/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