From f086bb6a39ae68ebdb4dca090b1b00473487fff7 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 24 Jun 2026 14:43:42 -0400 Subject: [PATCH 01/22] Delete deprecated modules --- .../FunctionProperties/Consequences.agda | 22 ---- .../FunctionProperties/Consequences/Core.agda | 17 --- .../Consequences/Propositional.agda | 17 --- src/Algebra/Operations/CommutativeMonoid.agda | 105 ------------------ src/Algebra/Operations/Ring.agda | 33 ------ src/Algebra/Operations/Semiring.agda | 31 ------ src/Data/AVL.agda | 20 ---- src/Data/AVL/Height.agda | 16 --- src/Data/AVL/Indexed.agda | 20 ---- src/Data/AVL/Indexed/WithK.agda | 22 ---- src/Data/AVL/IndexedMap.agda | 27 ----- src/Data/AVL/Key.agda | 20 ---- src/Data/AVL/Map.agda | 20 ---- src/Data/AVL/NonEmpty.agda | 19 ---- src/Data/AVL/NonEmpty/Propositional.agda | 23 ---- src/Data/AVL/Sets.agda | 20 ---- src/Data/AVL/Value.agda | 18 --- src/Data/List/Solver.agda | 27 ----- src/Foreign/Haskell/Maybe.agda | 59 ---------- src/Relation/Binary/OrderMorphism.agda | 83 -------------- src/Strict.agda | 20 ---- src/Text/Tree/Linear.agda | 16 --- 22 files changed, 655 deletions(-) delete mode 100644 src/Algebra/FunctionProperties/Consequences.agda delete mode 100644 src/Algebra/FunctionProperties/Consequences/Core.agda delete mode 100644 src/Algebra/FunctionProperties/Consequences/Propositional.agda delete mode 100644 src/Algebra/Operations/CommutativeMonoid.agda delete mode 100644 src/Algebra/Operations/Ring.agda delete mode 100644 src/Algebra/Operations/Semiring.agda delete mode 100644 src/Data/AVL.agda delete mode 100644 src/Data/AVL/Height.agda delete mode 100644 src/Data/AVL/Indexed.agda delete mode 100644 src/Data/AVL/Indexed/WithK.agda delete mode 100644 src/Data/AVL/IndexedMap.agda delete mode 100644 src/Data/AVL/Key.agda delete mode 100644 src/Data/AVL/Map.agda delete mode 100644 src/Data/AVL/NonEmpty.agda delete mode 100644 src/Data/AVL/NonEmpty/Propositional.agda delete mode 100644 src/Data/AVL/Sets.agda delete mode 100644 src/Data/AVL/Value.agda delete mode 100644 src/Data/List/Solver.agda delete mode 100644 src/Foreign/Haskell/Maybe.agda delete mode 100644 src/Relation/Binary/OrderMorphism.agda delete mode 100644 src/Strict.agda delete mode 100644 src/Text/Tree/Linear.agda diff --git a/src/Algebra/FunctionProperties/Consequences.agda b/src/Algebra/FunctionProperties/Consequences.agda deleted file mode 100644 index e28fe282d8..0000000000 --- a/src/Algebra/FunctionProperties/Consequences.agda +++ /dev/null @@ -1,22 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Bundles using (Setoid) -open import Relation.Binary.Definitions - using (Substitutive; Symmetric; Total) - -module Algebra.FunctionProperties.Consequences - {a ℓ} (S : Setoid a ℓ) where - -{-# WARNING_ON_IMPORT -"Algebra.FunctionProperties.Consequences was deprecated in v1.3. -Use Algebra.Consequences.Setoid instead." -#-} - -open import Algebra.Consequences.Setoid S public diff --git a/src/Algebra/FunctionProperties/Consequences/Core.agda b/src/Algebra/FunctionProperties/Consequences/Core.agda deleted file mode 100644 index fe7df6f770..0000000000 --- a/src/Algebra/FunctionProperties/Consequences/Core.agda +++ /dev/null @@ -1,17 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Algebra.FunctionProperties.Consequences.Core - {a} {A : Set a} where - -{-# WARNING_ON_IMPORT -"Algebra.FunctionProperties.Consequences.Core was deprecated in v1.3. -Use Algebra.Consequences.Base instead." -#-} - -open import Algebra.Consequences.Base public diff --git a/src/Algebra/FunctionProperties/Consequences/Propositional.agda b/src/Algebra/FunctionProperties/Consequences/Propositional.agda deleted file mode 100644 index 8d68750adf..0000000000 --- a/src/Algebra/FunctionProperties/Consequences/Propositional.agda +++ /dev/null @@ -1,17 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Algebra.FunctionProperties.Consequences.Propositional - {a} {A : Set a} where - -{-# WARNING_ON_IMPORT -"Algebra.FunctionProperties.Consequences.Propositional was deprecated in v1.3. -Use Algebra.Consequences.Propositional instead." -#-} - -open import Algebra.Consequences.Propositional {A = A} public diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda deleted file mode 100644 index 1f92b9e603..0000000000 --- a/src/Algebra/Operations/CommutativeMonoid.agda +++ /dev/null @@ -1,105 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Algebra -open import Data.List.Base as List using (List; []; _∷_; _++_) -open import Data.Fin.Base using (Fin; zero) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc) -open import Function.Base using (_∘_) -open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) - -module Algebra.Operations.CommutativeMonoid - {s₁ s₂} (CM : CommutativeMonoid s₁ s₂) - where - -{-# WARNING_ON_IMPORT -"Algebra.Operations.CommutativeMonoid was deprecated in v1.5. -Use Algebra.Properties.CommutativeMonoid.(Sum/Mult/Exp)(.TCOptimised) instead." -#-} - -open CommutativeMonoid CM - renaming - ( _∙_ to _+_ - ; ε to 0# - ; identityʳ to +-identityʳ - ; identityˡ to +-identityˡ - ; ∙-cong to +-cong - ; ∙-congˡ to +-congˡ - ; assoc to +-assoc - ) - -open import Relation.Binary.Reasoning.Setoid setoid - ------------------------------------------------------------------------- --- Multiplication - -infixr 8 _×_ _×′_ - -_×_ : ℕ → Carrier → Carrier -0 × x = 0# -suc n × x = x + (n × x) - -_×′_ : ℕ → Carrier → Carrier -0 ×′ x = 0# -1 ×′ x = x -suc n ×′ x = x + n ×′ x - ------------------------------------------------------------------------- --- Properties of _×_ - -×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_ -×-congʳ 0 x≈x′ = refl -×-congʳ (suc n) x≈x′ = +-cong x≈x′ (×-congʳ n x≈x′) - -×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_ -×-cong {u} ≡.refl x≈x′ = ×-congʳ u x≈x′ - --- _×_ is homomorphic with respect to _ℕ+_/_+_. - -×-homo-+ : ∀ c m n → (m ℕ.+ n) × c ≈ m × c + n × c -×-homo-+ c 0 n = sym (+-identityˡ (n × c)) -×-homo-+ c (suc m) n = begin - c + (m ℕ.+ n) × c ≈⟨ +-cong refl (×-homo-+ c m n) ⟩ - c + (m × c + n × c) ≈⟨ sym (+-assoc c (m × c) (n × c)) ⟩ - c + m × c + n × c ∎ - ------------------------------------------------------------------------- --- Properties of _×′_ - -1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x -1+×′ 0 x = sym (+-identityʳ x) -1+×′ (suc n) x = refl - --- _×_ and _×′_ are extensionally equal (up to the setoid --- equivalence). - -×≈×′ : ∀ n x → n × x ≈ n ×′ x -×≈×′ 0 x = refl -×≈×′ (suc n) x = begin - x + n × x ≈⟨ +-congˡ (×≈×′ n x) ⟩ - x + n ×′ x ≈⟨ sym (1+×′ n x) ⟩ - suc n ×′ x ∎ - --- _×′_ is homomorphic with respect to _ℕ+_/_+_. - -×′-homo-+ : ∀ c m n → (m ℕ.+ n) ×′ c ≈ m ×′ c + n ×′ c -×′-homo-+ c m n = begin - (m ℕ.+ n) ×′ c ≈⟨ sym (×≈×′ (m ℕ.+ n) c) ⟩ - (m ℕ.+ n) × c ≈⟨ ×-homo-+ c m n ⟩ - m × c + n × c ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩ - m ×′ c + n ×′ c ∎ - --- _×′_ preserves equality. - -×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_ -×′-cong {n} {_} {x} {y} ≡.refl x≈y = begin - n ×′ x ≈⟨ sym (×≈×′ n x) ⟩ - n × x ≈⟨ ×-congʳ n x≈y ⟩ - n × y ≈⟨ ×≈×′ n y ⟩ - n ×′ y ∎ diff --git a/src/Algebra/Operations/Ring.agda b/src/Algebra/Operations/Ring.agda deleted file mode 100644 index 7c0c9c6780..0000000000 --- a/src/Algebra/Operations/Ring.agda +++ /dev/null @@ -1,33 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Algebra - -module Algebra.Operations.Ring - {ℓ₁ ℓ₂} (ring : RawRing ℓ₁ ℓ₂) - where - -{-# WARNING_ON_IMPORT -"Algebra.Operations.Ring was deprecated in v1.5. -Use Algebra.Properties.Semiring.Exp(.TCOptimised) instead." -#-} - -open import Data.Nat.Base as ℕ using (ℕ; suc; zero) - -open RawRing ring - -infixr 8 _^_+1 -_^_+1 : Carrier → ℕ → Carrier -x ^ zero +1 = x -x ^ suc n +1 = (x ^ n +1) * x - -infixr 8 _^_ -_^_ : Carrier → ℕ → Carrier -x ^ zero = 1# -x ^ suc i = x ^ i +1 -{-# INLINE _^_ #-} diff --git a/src/Algebra/Operations/Semiring.agda b/src/Algebra/Operations/Semiring.agda deleted file mode 100644 index 5167f5adea..0000000000 --- a/src/Algebra/Operations/Semiring.agda +++ /dev/null @@ -1,31 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - --- Disabled to prevent warnings from deprecated --- Algebra.Operations.CommutativeMonoid -{-# OPTIONS --warning=noUserWarning #-} - -open import Algebra -import Algebra.Operations.CommutativeMonoid as MonoidOperations - -module Algebra.Operations.Semiring {s₁ s₂} (S : Semiring s₁ s₂) where - -{-# WARNING_ON_IMPORT -"Algebra.Operations.Semiring was deprecated in v1.5. -Use Algebra.Properties.Semiring.(Mult/Exp) instead." -#-} - -open Semiring S - ------------------------------------------------------------------------- --- Re-exports - -open MonoidOperations +-commutativeMonoid public -open import Algebra.Properties.Semiring.Exp S public -open import Algebra.Properties.Semiring.Mult S public - using (×1-homo-*) diff --git a/src/Data/AVL.agda b/src/Data/AVL.agda deleted file mode 100644 index d86636b8a6..0000000000 --- a/src/Data/AVL.agda +++ /dev/null @@ -1,20 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (StrictTotalOrder) - -module Data.AVL - {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) - where - -{-# WARNING_ON_IMPORT -"Data.AVL was deprecated in v1.4. -Use Data.Tree.AVL instead." -#-} - -open import Data.Tree.AVL strictTotalOrder public diff --git a/src/Data/AVL/Height.agda b/src/Data/AVL/Height.agda deleted file mode 100644 index d8dc3062d3..0000000000 --- a/src/Data/AVL/Height.agda +++ /dev/null @@ -1,16 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Data.AVL.Height where - -{-# WARNING_ON_IMPORT -"Data.AVL.Height was deprecated in v1.4. -Use Data.Tree.AVL.Height instead." -#-} - -open import Data.Tree.AVL.Height public diff --git a/src/Data/AVL/Indexed.agda b/src/Data/AVL/Indexed.agda deleted file mode 100644 index 954c759e24..0000000000 --- a/src/Data/AVL/Indexed.agda +++ /dev/null @@ -1,20 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (StrictTotalOrder) - -module Data.AVL.Indexed - {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where - - -{-# WARNING_ON_IMPORT -"Data.AVL.Indexed was deprecated in v1.4. -Use Data.Tree.AVL.Indexed instead." -#-} - -open import Data.Tree.AVL.Indexed strictTotalOrder public diff --git a/src/Data/AVL/Indexed/WithK.agda b/src/Data/AVL/Indexed/WithK.agda deleted file mode 100644 index 609fb7b45d..0000000000 --- a/src/Data/AVL/Indexed/WithK.agda +++ /dev/null @@ -1,22 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --with-K --safe #-} - -open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Structures using (IsStrictTotalOrder) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst) - -module Data.AVL.Indexed.WithK - {k r} (Key : Set k) {_<_ : Rel Key r} - (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where - -{-# WARNING_ON_IMPORT -"Data.AVL.Indexed.WithK was deprecated in v1.4. -Use Data.Tree.AVL.Indexed.WithK instead." -#-} - -open import Data.Tree.AVL.Indexed.WithK Key isStrictTotalOrder public diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda deleted file mode 100644 index 4f279d8265..0000000000 --- a/src/Data/AVL/IndexedMap.agda +++ /dev/null @@ -1,27 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Data.Product.Base using (∃) -open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Structures using (IsStrictTotalOrder) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst) -import Data.Tree.AVL.Value using (Value) - -module Data.AVL.IndexedMap - {i k v ℓ} - {Index : Set i} {Key : Index → Set k} (Value : Index → Set v) - {_<_ : Rel (∃ Key) ℓ} - (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) - where - -{-# WARNING_ON_IMPORT -"Data.AVL.IndexedMap was deprecated in v1.4. -Use Data.Tree.AVL.IndexedMap instead." -#-} - -open import Data.Tree.AVL.IndexedMap Value isStrictTotalOrder public diff --git a/src/Data/AVL/Key.agda b/src/Data/AVL/Key.agda deleted file mode 100644 index d367dca8ee..0000000000 --- a/src/Data/AVL/Key.agda +++ /dev/null @@ -1,20 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (StrictTotalOrder) - -module Data.AVL.Key - {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) - where - -{-# WARNING_ON_IMPORT -"Data.AVL.Key was deprecated in v1.4. -Use Data.Tree.AVL.Key instead." -#-} - -open import Data.Tree.AVL.Key strictTotalOrder public diff --git a/src/Data/AVL/Map.agda b/src/Data/AVL/Map.agda deleted file mode 100644 index ad23bddb6d..0000000000 --- a/src/Data/AVL/Map.agda +++ /dev/null @@ -1,20 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (StrictTotalOrder) - -module Data.AVL.Map - {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) - where - -{-# WARNING_ON_IMPORT -"Data.AVL.Map was deprecated in v1.4. -Use Data.Tree.AVL.Map instead." -#-} - -open import Data.Tree.AVL.Map strictTotalOrder public diff --git a/src/Data/AVL/NonEmpty.agda b/src/Data/AVL/NonEmpty.agda deleted file mode 100644 index 80bef71245..0000000000 --- a/src/Data/AVL/NonEmpty.agda +++ /dev/null @@ -1,19 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (StrictTotalOrder) - -module Data.AVL.NonEmpty - {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where - -{-# WARNING_ON_IMPORT -"Data.AVL.NonEmpty was deprecated in v1.4. -Use Data.Tree.AVL.NonEmpty instead." -#-} - -open import Data.Tree.AVL.NonEmpty strictTotalOrder public diff --git a/src/Data/AVL/NonEmpty/Propositional.agda b/src/Data/AVL/NonEmpty/Propositional.agda deleted file mode 100644 index 9cb176a75a..0000000000 --- a/src/Data/AVL/NonEmpty/Propositional.agda +++ /dev/null @@ -1,23 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Core using (Rel) -open import Relation.Binary.Structures using (IsStrictTotalOrder) -open import Relation.Binary.Bundles using (StrictTotalOrder) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst) - -module Data.AVL.NonEmpty.Propositional - {k r} {Key : Set k} {_<_ : Rel Key r} - (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where - -{-# WARNING_ON_IMPORT -"Data.AVL.NonEmpty.Propositional was deprecated in v1.4. -Use Data.Tree.AVL.NonEmpty.Propositonal instead." -#-} - -open import Data.Tree.AVL.NonEmpty.Propositional isStrictTotalOrder public diff --git a/src/Data/AVL/Sets.agda b/src/Data/AVL/Sets.agda deleted file mode 100644 index 88cd0172ff..0000000000 --- a/src/Data/AVL/Sets.agda +++ /dev/null @@ -1,20 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (StrictTotalOrder) - -module Data.AVL.Sets - {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) - where - -{-# WARNING_ON_IMPORT -"Data.AVL.Sets was deprecated in v1.4. -Use Data.Tree.AVL.Sets instead." -#-} - -open import Data.Tree.AVL.Sets strictTotalOrder public diff --git a/src/Data/AVL/Value.agda b/src/Data/AVL/Value.agda deleted file mode 100644 index 2085bb7e64..0000000000 --- a/src/Data/AVL/Value.agda +++ /dev/null @@ -1,18 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Relation.Binary.Bundles using (Setoid) - -module Data.AVL.Value {a ℓ} (S : Setoid a ℓ) where - -{-# WARNING_ON_IMPORT -"Data.AVL.Value was deprecated in v1.4. -Use Data.Tree.AVL.Value instead." -#-} - -open import Data.Tree.AVL.Value S public diff --git a/src/Data/List/Solver.agda b/src/Data/List/Solver.agda deleted file mode 100644 index 585d35688f..0000000000 --- a/src/Data/List/Solver.agda +++ /dev/null @@ -1,27 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - --- Disabled to prevent warnings from deprecated monoid solver -{-# OPTIONS --warning=noUserWarning #-} - -module Data.List.Solver where - -{-# WARNING_ON_IMPORT -"Data.List.Solver was deprecated in v1.3. -Use the new reflective Tactic.MonoidSolver instead." -#-} - -import Algebra.Solver.Monoid as Solver -open import Data.List.Properties using (++-monoid) - ------------------------------------------------------------------------- --- A module for automatically solving propositional equivalences --- containing _++_ - -module ++-Solver {a} {A : Set a} = - Solver (++-monoid A) renaming (id to nil) diff --git a/src/Foreign/Haskell/Maybe.agda b/src/Foreign/Haskell/Maybe.agda deleted file mode 100644 index 14a111e5af..0000000000 --- a/src/Foreign/Haskell/Maybe.agda +++ /dev/null @@ -1,59 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. Please use the builtin Maybe instead. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K #-} - -module Foreign.Haskell.Maybe where - -open import Level using (Level; _⊔_) -open import Data.Maybe.Base as Data using (just; nothing) - -private - variable - a : Level - A : Set a - ------------------------------------------------------------------------- --- Definition - -data Maybe (A : Set a) : Set a where - just : A → Maybe A - nothing : Maybe A - -{-# FOREIGN GHC type AgdaMaybe l a = Maybe a #-} -{-# COMPILE GHC Maybe = data AgdaMaybe (Just | Nothing) #-} - ------------------------------------------------------------------------- --- Conversion - -toForeign : Data.Maybe A → Maybe A -toForeign (just x) = just x -toForeign nothing = nothing - -fromForeign : Maybe A → Data.Maybe A -fromForeign (just x) = just x -fromForeign nothing = nothing - - -{-# WARNING_ON_IMPORT -"Warning: Foreign.Haskell.Maybe was deprecated in v1.4. -Maybe is now an Agda builtin and does not need library support." -#-} - -{-# WARNING_ON_USAGE Maybe -"Warning: Foreign.Haskell.Maybe's Maybe was deprecated in v1.4. -Maybe is now an Agda builtin and does not need library support." -#-} - -{-# WARNING_ON_USAGE toForeign -"Warning: toForeign was deprecated in v1.4. -Maybe is now an Agda builtin and does not need library support." -#-} - -{-# WARNING_ON_USAGE fromForeign -"Warning: fromForeign was deprecated in v1.4. -Maybe is now an Agda builtin and does not need library support." -#-} diff --git a/src/Relation/Binary/OrderMorphism.agda b/src/Relation/Binary/OrderMorphism.agda deleted file mode 100644 index f99b58e3f9..0000000000 --- a/src/Relation/Binary/OrderMorphism.agda +++ /dev/null @@ -1,83 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. Please use `Relation.Binary.Morphism` --- instead. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Relation.Binary.OrderMorphism where - -{-# WARNING_ON_IMPORT -"Relation.Binary.OrderMorphism was deprecated in v1.5. -Use Relation.Binary.Morphism.Bundles instead." -#-} - -open import Relation.Binary.Core using (_=[_]⇒_) -open import Relation.Binary.Bundles using (Poset; DecTotalOrder) -open Poset -import Function.Base as F -open import Level - -record _⇒-Poset_ {p₁ p₂ p₃ p₄ p₅ p₆} - (P₁ : Poset p₁ p₂ p₃) - (P₂ : Poset p₄ p₅ p₆) : Set (p₁ ⊔ p₃ ⊔ p₄ ⊔ p₆) where - field - fun : Carrier P₁ → Carrier P₂ - monotone : _≤_ P₁ =[ fun ]⇒ _≤_ P₂ - - -_⇒-DTO_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} → - DecTotalOrder p₁ p₂ p₃ → - DecTotalOrder p₄ p₅ p₆ → Set _ -DTO₁ ⇒-DTO DTO₂ = poset DTO₁ ⇒-Poset poset DTO₂ - where open DecTotalOrder - -open _⇒-Poset_ - -id : ∀ {p₁ p₂ p₃} {P : Poset p₁ p₂ p₃} → P ⇒-Poset P -id = record - { fun = F.id - ; monotone = F.id - } - -_∘_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉} - {P₁ : Poset p₁ p₂ p₃} - {P₂ : Poset p₄ p₅ p₆} - {P₃ : Poset p₇ p₈ p₉} → - P₂ ⇒-Poset P₃ → P₁ ⇒-Poset P₂ → P₁ ⇒-Poset P₃ -f ∘ g = record - { fun = F._∘_ (fun f) (fun g) - ; monotone = F._∘_ (monotone f) (monotone g) - } - -const : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} - {P₁ : Poset p₁ p₂ p₃} - {P₂ : Poset p₄ p₅ p₆} → - Carrier P₂ → P₁ ⇒-Poset P₂ -const {P₂ = P₂} x = record - { fun = F.const x - ; monotone = F.const (refl P₂) - } - -{-# WARNING_ON_USAGE _⇒-Poset_ -"Warning: _⇒-Poset_ was deprecated in v1.5. -Please use `IsOrderHomomorphism` from `Relation.Binary.Morphism.Structures` instead." -#-} -{-# WARNING_ON_USAGE _⇒-DTO_ -"Warning: _⇒-DTO_ was deprecated in v1.5. -Please use `IsOrderHomomorphism` from `Relation.Binary.Morphism.Structures` instead." -#-} -{-# WARNING_ON_USAGE id -"Warning: id was deprecated in v1.5. -Please use `issOrderHomomorphism` from `Relation.Binary.Morphism.Construct.Constant` instead." -#-} -{-# WARNING_ON_USAGE _∘_ -"Warning: _∘_ was deprecated in v1.5. -Please use `isOrderHomomorphism` from `Relation.Binary.Morphism.Construct.Composition` instead." -#-} -{-# WARNING_ON_USAGE const -"Warning: const was deprecated in v1.5. -Please use `isOrderHomomorphism` from `Relation.Binary.Morphism.Construct.Constant` instead." -#-} diff --git a/src/Strict.agda b/src/Strict.agda deleted file mode 100644 index d688c13fd1..0000000000 --- a/src/Strict.agda +++ /dev/null @@ -1,20 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED, please use `Function.Strict` directly. ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -module Strict where - -{-# WARNING_ON_IMPORT -"Strict was deprecated in v1.8. -Use `Function.Strict instead (also re-exported by `Function`)." -#-} - -open import Function.Strict public - using - ( force ; force-≡ ; force′ ; force′-≡ - ; seq ; seq-≡ - ) diff --git a/src/Text/Tree/Linear.agda b/src/Text/Tree/Linear.agda deleted file mode 100644 index 9e1596bb6a..0000000000 --- a/src/Text/Tree/Linear.agda +++ /dev/null @@ -1,16 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- This module is DEPRECATED. Please use the Data.Tree.Rose.Show module --- directly ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --sized-types #-} - -module Text.Tree.Linear where - -open import Data.Tree.Rose.Show public using (display) - -{-# WARNING_ON_IMPORT -"Text.Tree.Linear was deprecated in v1.6. Use Data.Tree.Rose.Show instead." -#-} From 28f902e5514f09d431faf670f1f744cc6c514488 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 24 Jun 2026 14:44:07 -0400 Subject: [PATCH 02/22] Remove deleted modules from 'unsafeModules' --- GenerateEverything.hs | 2 -- 1 file changed, 2 deletions(-) diff --git a/GenerateEverything.hs b/GenerateEverything.hs index e8986484b1..b4356c6bf0 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -64,7 +64,6 @@ unsafeModules = map modToFile , "Foreign.Haskell" , "Foreign.Haskell.Coerce" , "Foreign.Haskell.Either" - , "Foreign.Haskell.Maybe" , "Foreign.Haskell.List.NonEmpty" , "Foreign.Haskell.Pair" , "IO" @@ -183,7 +182,6 @@ sizedTypesModules = map modToFile , "Data.Trie.NonEmpty" , "Relation.Unary.Sized" , "Size" - , "Text.Tree.Linear" ] isSizedTypesModule :: FilePath -> Bool From 07f12b7ed43c2fdc3fa102bfd6837ca568a509c7 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 24 Jun 2026 14:58:19 -0400 Subject: [PATCH 03/22] Remove useless pattern attribute --- src/Reflection/AST/Traversal.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda index e2a96b4bc2..c99965800d 100644 --- a/src/Reflection/AST/Traversal.agda +++ b/src/Reflection/AST/Traversal.agda @@ -27,7 +27,6 @@ open RawApplicative AppF -- compute the length of the context everytime it's needed. record Cxt : Set where constructor _,_ - pattern field len : ℕ context : List (String × Arg Term) From d04ccc6d4d5780df861b733a498ef4a4a460f896 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 24 Jun 2026 15:08:54 -0400 Subject: [PATCH 04/22] Add lemma of congruence on IsRelHomomorphism --- .../Construct/PropositionalEquality.agda | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda diff --git a/src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda b/src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda new file mode 100644 index 0000000000..fdeaff2bd7 --- /dev/null +++ b/src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda @@ -0,0 +1,16 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Propositional Equality Lemmas over Morphisms +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Agda.Builtin.Equality using (_≡_) +open import Relation.Binary.PropositionalEquality.Core using (cong) +open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism) + +module Relation.Binary.Morphism.Construct.PropositionalEquality where + +cong-IsRelHomomorphism : ∀ {a b} {A : Set a} {B : Set b} → (f : A → B) → IsRelHomomorphism _≡_ _≡_ f +cong-IsRelHomomorphism f .IsRelHomomorphism.cong = cong f From cd9d5ce2aeb1ffd99d78caa55504a549da6773e3 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Wed, 24 Jun 2026 15:09:16 -0400 Subject: [PATCH 05/22] Remove stale (v1.x) names and their associated warnings --- src/Algebra/Morphism.agda | 178 ------------------ src/Algebra/Morphism/Definitions.agda | 16 -- src/Algebra/Properties/BooleanAlgebra.agda | 25 --- .../Properties/DistributiveLattice.agda | 23 --- src/Algebra/Properties/Lattice.agda | 35 ---- .../Solver/Ring/AlmostCommutativeRing.agda | 4 +- src/Data/Char.agda | 2 +- src/Data/Char/Properties.agda | 118 +----------- src/Data/Fin/Properties.agda | 8 - src/Data/Fin/Subset/Properties.agda | 16 -- src/Data/Integer.agda | 28 --- src/Data/Integer/Properties.agda | 101 ---------- src/Data/List/Base.agda | 10 - .../Fresh/Membership/Setoid/Properties.agda | 15 -- src/Data/List/NonEmpty.agda | 23 --- .../Subset/Propositional/Properties.agda | 66 ------- .../Binary/Subset/Setoid/Properties.agda | 13 -- src/Data/List/Relation/Unary/All.agda | 14 -- .../List/Relation/Unary/All/Properties.agda | 8 - src/Data/List/Relation/Unary/Any.agda | 15 -- src/Data/Nat/Binary/Properties.agda | 28 --- src/Data/Nat/Properties.agda | 101 +--------- src/Data/Rational.agda | 21 --- .../Rational/Unnormalised/Properties.agda | 8 - src/Data/Record.agda | 1 + src/Data/Vec/Relation/Unary/All.agda | 7 - src/Data/Vec/Relation/Unary/Any.agda | 6 - src/Function/Base.agda | 8 - src/Induction/WellFounded.agda | 115 ----------- src/Reflection.agda | 168 ----------------- src/Relation/Binary/Bundles.agda | 10 - src/Relation/Binary/Consequences.agda | 106 ----------- .../Binary/Construct/Closure/Reflexive.agda | 16 -- .../Binary/Construct/Closure/Transitive.agda | 14 -- .../Binary/Construct/StrictToNonStrict.agda | 16 -- .../Binary/Reasoning/Base/Partial.agda | 18 -- .../Core/AlmostCommutativeRing.agda | 2 +- 37 files changed, 12 insertions(+), 1351 deletions(-) diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda index 9ed266bc42..d430d5ac04 100644 --- a/src/Algebra/Morphism.agda +++ b/src/Algebra/Morphism.agda @@ -28,181 +28,3 @@ module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) w open MorphismDefinitions A B _≈_ public open import Algebra.Morphism.Structures public - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new definitions re-exported from --- `Algebra.Morphism.Structures` as continuing support for the below is --- no guaranteed. - --- Version 1.5 - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : Semigroup c₁ ℓ₁) - (To : Semigroup c₂ ℓ₂) where - - private - module F = Semigroup From - module T = Semigroup To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsSemigroupMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_ - ∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_ - - IsSemigroupMorphism-syntax = IsSemigroupMorphism - syntax IsSemigroupMorphism-syntax From To F = F Is From -Semigroup⟶ To - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : Monoid c₁ ℓ₁) - (To : Monoid c₂ ℓ₂) where - - private - module F = Monoid From - module T = Monoid To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsMonoidMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧ - ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε - - open IsSemigroupMorphism sm-homo public - - IsMonoidMorphism-syntax = IsMonoidMorphism - syntax IsMonoidMorphism-syntax From To F = F Is From -Monoid⟶ To - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : CommutativeMonoid c₁ ℓ₁) - (To : CommutativeMonoid c₂ ℓ₂) where - - private - module F = CommutativeMonoid From - module T = CommutativeMonoid To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧ - - open IsMonoidMorphism mn-homo public - - IsCommutativeMonoidMorphism-syntax = IsCommutativeMonoidMorphism - syntax IsCommutativeMonoidMorphism-syntax From To F = F Is From -CommutativeMonoid⟶ To - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : IdempotentCommutativeMonoid c₁ ℓ₁) - (To : IdempotentCommutativeMonoid c₂ ℓ₂) where - - private - module F = IdempotentCommutativeMonoid From - module T = IdempotentCommutativeMonoid To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧ - - open IsMonoidMorphism mn-homo public - - isCommutativeMonoidMorphism : - IsCommutativeMonoidMorphism F.commutativeMonoid T.commutativeMonoid ⟦_⟧ - isCommutativeMonoidMorphism = record { mn-homo = mn-homo } - - IsIdempotentCommutativeMonoidMorphism-syntax = IsIdempotentCommutativeMonoidMorphism - syntax IsIdempotentCommutativeMonoidMorphism-syntax From To F = F Is From -IdempotentCommutativeMonoid⟶ To - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : Group c₁ ℓ₁) - (To : Group c₂ ℓ₂) where - - private - module F = Group From - module T = Group To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsGroupMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧ - - open IsMonoidMorphism mn-homo public - - ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹ - ⁻¹-homo x = let open ≈-Reasoning T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin - ⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩ - ⟦ x F.⁻¹ F.∙ x ⟧ ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩ - ⟦ F.ε ⟧ ≈⟨ ε-homo ⟩ - T.ε ∎ - - IsGroupMorphism-syntax = IsGroupMorphism - syntax IsGroupMorphism-syntax From To F = F Is From -Group⟶ To - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : AbelianGroup c₁ ℓ₁) - (To : AbelianGroup c₂ ℓ₂) where - - private - module F = AbelianGroup From - module T = AbelianGroup To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsAbelianGroupMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - gp-homo : IsGroupMorphism F.group T.group ⟦_⟧ - - open IsGroupMorphism gp-homo public - - IsAbelianGroupMorphism-syntax = IsAbelianGroupMorphism - syntax IsAbelianGroupMorphism-syntax From To F = F Is From -AbelianGroup⟶ To - -module _ {c₁ ℓ₁ c₂ ℓ₂} - (From : Ring c₁ ℓ₁) - (To : Ring c₂ ℓ₂) where - - private - module F = Ring From - module T = Ring To - open Definitions F.Carrier T.Carrier T._≈_ - - record IsRingMorphism (⟦_⟧ : Morphism) : - Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where - field - +-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup - *-mn-homo : ⟦_⟧ Is F.*-monoid -Monoid⟶ T.*-monoid - - IsRingMorphism-syntax = IsRingMorphism - syntax IsRingMorphism-syntax From To F = F Is From -Ring⟶ To - -{-# WARNING_ON_USAGE IsSemigroupMorphism -"Warning: IsSemigroupMorphism was deprecated in v1.5. -Please use IsMagmaHomomorphism instead." -#-} -{-# WARNING_ON_USAGE IsMonoidMorphism -"Warning: IsMonoidMorphism was deprecated in v1.5. -Please use IsMonoidHomomorphism instead." -#-} -{-# WARNING_ON_USAGE IsCommutativeMonoidMorphism -"Warning: IsCommutativeMonoidMorphism was deprecated in v1.5. -Please use IsMonoidHomomorphism instead." -#-} -{-# WARNING_ON_USAGE IsIdempotentCommutativeMonoidMorphism -"Warning: IsIdempotentCommutativeMonoidMorphism was deprecated in v1.5. -Please use IsMonoidHomomorphism instead." -#-} -{-# WARNING_ON_USAGE IsGroupMorphism -"Warning: IsGroupMorphism was deprecated in v1.5. -Please use IsGroupHomomorphism instead." -#-} -{-# WARNING_ON_USAGE IsAbelianGroupMorphism -"Warning: IsAbelianGroupMorphism was deprecated in v1.5. -Please use IsGroupHomomorphism instead." -#-} diff --git a/src/Algebra/Morphism/Definitions.agda b/src/Algebra/Morphism/Definitions.agda index ead9a123fc..0c3dc9514c 100644 --- a/src/Algebra/Morphism/Definitions.agda +++ b/src/Algebra/Morphism/Definitions.agda @@ -28,19 +28,3 @@ Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧) Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Set _ Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧) - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.3 - -Morphism : Set _ -Morphism = A → B - -{-# WARNING_ON_USAGE Morphism -"Warning: Morphism was deprecated in v1.3. -Please use the standard function notation (e.g. A → B) instead." -#-} diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda index 1b9c7ba08a..617b780dd4 100644 --- a/src/Algebra/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Properties/BooleanAlgebra.agda @@ -30,28 +30,3 @@ open import Algebra.Structures _≈_ open import Relation.Binary open import Function.Bundles using (module Equivalence; _⇔_) open import Data.Product.Base using (_,_) - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.4 - -replace-equality : {_≈′_ : Rel Carrier b₂} → - (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → - BooleanAlgebra _ _ -replace-equality {_≈′_} ≈⇔≈′ = record - { isBooleanAlgebra = record - { isDistributiveLattice = DistributiveLattice.isDistributiveLattice - (DistribLatticeProperties.replace-equality distributiveLattice ≈⇔≈′) - ; ∨-complement = ((λ x → to (∨-complementˡ x)) , λ x → to (∨-complementʳ x)) - ; ∧-complement = ((λ x → to (∧-complementˡ x)) , λ x → to (∧-complementʳ x)) - ; ¬-cong = λ i≈j → to (¬-cong (from i≈j)) - } - } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) -{-# WARNING_ON_USAGE replace-equality -"Warning: replace-equality was deprecated in v1.4. -Please use isBooleanAlgebra from `Algebra.Construct.Subst.Equality` instead." -#-} diff --git a/src/Algebra/Properties/DistributiveLattice.agda b/src/Algebra/Properties/DistributiveLattice.agda index 9b3441c425..d2069bf20b 100644 --- a/src/Algebra/Properties/DistributiveLattice.agda +++ b/src/Algebra/Properties/DistributiveLattice.agda @@ -27,26 +27,3 @@ Use Algebra.Lattice.Properties.DistributiveLattice instead." open DistributiveLattice DL open import Algebra.Lattice.Properties.DistributiveLattice DL public import Algebra.Properties.Lattice as LatticeProperties - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.4 - -replace-equality : {_≈′_ : Rel Carrier ℓ₂} → - (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → - DistributiveLattice _ _ -replace-equality {_≈′_} ≈⇔≈′ = record - { isDistributiveLattice = isDistributiveLatticeʳʲᵐ (record - { isLattice = Lattice.isLattice - (LatticeProperties.replace-equality lattice ≈⇔≈′) - ; ∨-distribʳ-∧ = λ x y z → to (∨-distribʳ-∧ x y z) - }) - } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) -{-# WARNING_ON_USAGE replace-equality -"Warning: replace-equality was deprecated in v1.4. -Please use isDistributiveLattice from `Algebra.Construct.Subst.Equality` instead." -#-} diff --git a/src/Algebra/Properties/Lattice.agda b/src/Algebra/Properties/Lattice.agda index 02ff07c4c7..30bd6ace7f 100644 --- a/src/Algebra/Properties/Lattice.agda +++ b/src/Algebra/Properties/Lattice.agda @@ -21,38 +21,3 @@ open import Algebra.Lattice.Properties.Lattice L public "Algebra.Properties.Lattice was deprecated in v2.0. Use Algebra.Lattice.Properties.Lattice instead." #-} - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - -open Lattice L - --- Version 1.4 - -replace-equality : {_≈′_ : Rel Carrier l₂} → - (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → Lattice _ _ -replace-equality {_≈′_} ≈⇔≈′ = record - { isLattice = record - { isEquivalence = record - { refl = to refl - ; sym = λ x≈y → to (sym (from x≈y)) - ; trans = λ x≈y y≈z → to (trans (from x≈y) (from y≈z)) - } - ; ∨-comm = λ x y → to (∨-comm x y) - ; ∨-assoc = λ x y z → to (∨-assoc x y z) - ; ∨-cong = λ x≈y u≈v → to (∨-cong (from x≈y) (from u≈v)) - ; ∧-comm = λ x y → to (∧-comm x y) - ; ∧-assoc = λ x y z → to (∧-assoc x y z) - ; ∧-cong = λ x≈y u≈v → to (∧-cong (from x≈y) (from u≈v)) - ; absorptive = (λ x y → to (∨-absorbs-∧ x y)) - , (λ x y → to (∧-absorbs-∨ x y)) - } - } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y}) -{-# WARNING_ON_USAGE replace-equality -"Warning: replace-equality was deprecated in v1.4. -Please use isLattice from `Algebra.Construct.Subst.Equality` instead." -#-} diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda index 9156e33696..0933577d80 100644 --- a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda +++ b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda @@ -14,7 +14,7 @@ open import Algebra using open import Algebra.Structures using (IsCommutativeSemiring) open import Algebra.Definitions using (Congruent₁; Congruent₂) import Algebra.Morphism.Definitions as MorphismDefinitions using - (Homomorphic₀; Homomorphic₁; Homomorphic₂; Morphism) + (Homomorphic₀; Homomorphic₁; Homomorphic₂) open import Function.Base using (id) open import Level using (suc; _⊔_) open import Relation.Binary.Core using (Rel) @@ -88,7 +88,7 @@ record _-Raw-AlmostCommutative⟶_ module T = AlmostCommutativeRing To open MorphismDefinitions F.Carrier T.Carrier T._≈_ field - ⟦_⟧ : Morphism + ⟦_⟧ : F.Carrier → T.Carrier +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_ *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_ -‿homo : Homomorphic₁ ⟦_⟧ F.-_ T.-_ diff --git a/src/Data/Char.agda b/src/Data/Char.agda index 22e32f45bf..98781dac13 100644 --- a/src/Data/Char.agda +++ b/src/Data/Char.agda @@ -13,4 +13,4 @@ module Data.Char where open import Data.Char.Base public open import Data.Char.Properties - using (_≈?_; _≟_; _≡?_; _ = neg-mono-< -{-# WARNING_ON_USAGE neg-mono-<-> -"Warning: neg-mono-<-> was deprecated in v1.5. -Please use neg-mono-< instead." -#-} - -neg-mono-≤-≥ = neg-mono-≤ -{-# WARNING_ON_USAGE neg-mono-≤-≥ -"Warning: neg-mono-≤-≥ was deprecated in v1.5. -Please use neg-mono-≤ instead." -#-} - -*-monoʳ-≤-non-neg = *-monoʳ-≤-nonNeg -{-# WARNING_ON_USAGE *-monoʳ-≤-non-neg -"Warning: *-monoʳ-≤-non-neg was deprecated in v1.5. -Please use *-monoʳ-≤-nonNeg instead." -#-} - -*-monoˡ-≤-non-neg = *-monoˡ-≤-nonNeg -{-# WARNING_ON_USAGE *-monoˡ-≤-non-neg -"Warning: *-monoˡ-≤-non-neg deprecated in v1.5. -Please use *-monoˡ-≤-nonNeg instead." -#-} - -*-cancelˡ-<-non-neg = *-cancelˡ-<-nonNeg -{-# WARNING_ON_USAGE *-cancelˡ-<-non-neg -"Warning: *-cancelˡ-<-non-neg was deprecated in v1.5. -Please use *-cancelˡ-<-nonNeg instead." -#-} - -*-cancelʳ-<-non-neg = *-cancelʳ-<-nonNeg -{-# WARNING_ON_USAGE *-cancelʳ-<-non-neg -"Warning: *-cancelʳ-<-non-neg was deprecated in v1.5. -Please use *-cancelʳ-<-nonNeg instead." -#-} - --- Version 1.6 - -m≤n⇒m⊓n≡m = i≤j⇒i⊓j≡i -{-# WARNING_ON_USAGE m≤n⇒m⊓n≡m -"Warning: m≤n⇒m⊓n≡m was deprecated in v1.6 -Please use i≤j⇒i⊓j≡i instead." -#-} -m⊓n≡m⇒m≤n = i⊓j≡i⇒i≤j -{-# WARNING_ON_USAGE m⊓n≡m⇒m≤n -"Warning: m≤n⇒m⊓n≡m was deprecated in v1.6 -Please use i⊓j≡i⇒i≤j instead." -#-} -m≥n⇒m⊓n≡n = i≥j⇒i⊓j≡j -{-# WARNING_ON_USAGE m≥n⇒m⊓n≡n -"Warning: m≥n⇒m⊓n≡n was deprecated in v1.6 -Please use i≥j⇒i⊓j≡j instead." -#-} -m⊓n≡n⇒m≥n = i⊓j≡j⇒j≤i -{-# WARNING_ON_USAGE m⊓n≡n⇒m≥n -"Warning: m⊓n≡n⇒m≥n was deprecated in v1.6 -Please use i⊓j≡j⇒j≤i instead." -#-} -m⊓n≤n = i⊓j≤j -{-# WARNING_ON_USAGE m⊓n≤n -"Warning: m⊓n≤n was deprecated in v1.6 -Please use i⊓j≤j instead." -#-} -m⊓n≤m = i⊓j≤i -{-# WARNING_ON_USAGE m⊓n≤m -"Warning: m⊓n≤m was deprecated in v1.6 -Please use i⊓j≤i instead." -#-} -m≤n⇒m⊔n≡n = i≤j⇒i⊔j≡j -{-# WARNING_ON_USAGE m≤n⇒m⊔n≡n -"Warning: m≤n⇒m⊔n≡n was deprecated in v1.6 -Please use i≤j⇒i⊔j≡j instead." -#-} -m⊔n≡n⇒m≤n = i⊔j≡j⇒i≤j -{-# WARNING_ON_USAGE m⊔n≡n⇒m≤n -"Warning: m⊔n≡n⇒m≤n was deprecated in v1.6 -Please use i⊔j≡j⇒i≤j instead." -#-} -m≥n⇒m⊔n≡m = i≥j⇒i⊔j≡i -{-# WARNING_ON_USAGE m≥n⇒m⊔n≡m -"Warning: m≥n⇒m⊔n≡m was deprecated in v1.6 -Please use i≥j⇒i⊔j≡i instead." -#-} -m⊔n≡m⇒m≥n = i⊔j≡i⇒j≤i -{-# WARNING_ON_USAGE m⊔n≡m⇒m≥n -"Warning: m⊔n≡m⇒m≥n was deprecated in v1.6 -Please use i⊔j≡i⇒j≤i instead." -#-} -m≤m⊔n = i≤i⊔j -{-# WARNING_ON_USAGE m≤m⊔n -"Warning: m≤m⊔n was deprecated in v1.6 -Please use i≤i⊔j instead." -#-} -n≤m⊔n = i≤j⊔i -{-# WARNING_ON_USAGE n≤m⊔n -"Warning: n≤m⊔n was deprecated in v1.6 -Please use i≤j⊔i instead." -#-} - -- Version 2.0 +-pos-monoʳ-≤ : ∀ n → (_+_ (+ n)) Preserves _≤_ ⟶ _≤_ diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 548e0bd827..79b87608d3 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -526,16 +526,6 @@ module _ (A : Set a) where -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 1.4 - -infixl 5 _∷ʳ'_ -_∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x) -_∷ʳ'_ = InitLast._∷ʳ′_ -{-# WARNING_ON_USAGE _∷ʳ'_ -"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4. -Please use _∷ʳ′_ (ending in a prime) instead." -#-} - -- Version 2.0 infixl 5 _─_ diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda index e55a546a83..95817d9c7d 100644 --- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda +++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda @@ -158,18 +158,3 @@ All[x≉]-∉ : All (x ≉_) xs → x ∉ xs All[x≉]-∉ [] () All[x≉]-∉ (p ∷ ps) (here x≈y) = p x≈y All[x≉]-∉ (p ∷ ps) (there x∈ys) = All[x≉]-∉ ps x∈ys - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.4 - -≈-subst-∈ = ∈-resp-≈ -{-# WARNING_ON_USAGE ≈-subst-∈ -"Warning: ≈-subst-∈ was deprecated in v1.4. -Please use ∈-resp-≈ instead." -#-} diff --git a/src/Data/List/NonEmpty.agda b/src/Data/List/NonEmpty.agda index e2f1720630..a7590018a0 100644 --- a/src/Data/List/NonEmpty.agda +++ b/src/Data/List/NonEmpty.agda @@ -15,26 +15,3 @@ open import Data.List.Base as List using (List) -- Re-export basic type and operations open import Data.List.NonEmpty.Base public - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - -private - variable - a : Level - A : Set a - --- Version 1.4 - -infixl 5 _∷ʳ'_ - -_∷ʳ'_ : (xs : List A) (x : A) → SnocView (xs ∷ʳ x) -_∷ʳ'_ = SnocView._∷ʳ′_ -{-# WARNING_ON_USAGE _∷ʳ'_ -"Warning: _∷ʳ'_ (ending in an apostrophe) was deprecated in v1.4. -Please use _∷ʳ′_ (ending in a prime) instead." -#-} diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda index adfcf3d357..14c19033ee 100644 --- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda @@ -283,69 +283,3 @@ module _ {P : Pred A p} (P? : Decidable P) where filter⁺′ : P ⋐ Q → ∀ {xs ys} → xs ⊆ ys → filter P? xs ⊆ filter Q? ys filter⁺′ = Subset.filter⁺′ (setoid A) P? (resp P) Q? (resp Q) - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- - --- Version 1.5 - -mono = Any-resp-⊆ -{-# WARNING_ON_USAGE mono -"Warning: mono was deprecated in v1.5. -Please use Any-resp-⊆ instead." -#-} -map-mono = map⁺ -{-# WARNING_ON_USAGE map-mono -"Warning: map-mono was deprecated in v1.5. -Please use map⁺ instead." -#-} -infix 4 _++-mono_ -_++-mono_ = ++⁺ -{-# WARNING_ON_USAGE _++-mono_ -"Warning: _++-mono_ was deprecated in v1.5. -Please use ++⁺ instead." -#-} -concat-mono = concat⁺ -{-# WARNING_ON_USAGE concat-mono -"Warning: concat-mono was deprecated in v1.5. -Please use concat⁺ instead." -#-} ->>=-mono = >>=⁺ -{-# WARNING_ON_USAGE >>=-mono -"Warning: >>=-mono was deprecated in v1.5. -Please use >>=⁺ instead." -#-} -infix 4 _⊛-mono_ -_⊛-mono_ = ⊛⁺ -{-# WARNING_ON_USAGE _⊛-mono_ -"Warning: _⊛-mono_ was deprecated in v1.5. -Please use ⊛⁺ instead." -#-} -infix 4 _⊗-mono_ -_⊗-mono_ = ⊗⁺ -{-# WARNING_ON_USAGE _⊗-mono_ -"Warning: _⊗-mono_ was deprecated in v1.5. -Please use ⊗⁺ instead." -#-} -any-mono = any⁺ -{-# WARNING_ON_USAGE any-mono -"Warning: any-mono was deprecated in v1.5. -Please use any⁺ instead." -#-} -map-with-∈-mono = mapWith∈⁺ -{-# WARNING_ON_USAGE map-with-∈-mono -"Warning: map-with-∈-mono was deprecated in v1.5. -Please use mapWith∈⁺ instead." -#-} -map-with-∈⁺ = mapWith∈⁺ -{-# WARNING_ON_USAGE map-with-∈⁺ -"Warning: map-with-∈⁺ was deprecated in v2.0. -Please use mapWith∈⁺ instead." -#-} -filter⁺ = filter-⊆ -{-# WARNING_ON_USAGE filter⁺ -"Warning: filter⁺ was deprecated in v1.5. -Please use filter-⊆ instead." -#-} diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 8fa6b0cb61..7256294dab 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -338,16 +338,3 @@ module _ (S : Setoid a ℓ) where applyUpTo⁺ : ∀ (f : ℕ → A) {m n} → m ≤ n → applyUpTo f m ⊆ applyUpTo f n applyUpTo⁺ _ (s≤s m≤n) (here f≡f[0]) = here f≡f[0] applyUpTo⁺ _ (s≤s m≤n) (there v∈xs) = there (applyUpTo⁺ _ m≤n v∈xs) - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- - --- Version 1.5 - -filter⁺ = filter-⊆ -{-# WARNING_ON_USAGE filter⁺ -"Warning: filter⁺ was deprecated in v1.5. -Please use filter-⊆ instead." -#-} diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda index b29002d1c2..72d3ffc2c8 100644 --- a/src/Data/List/Relation/Unary/All.agda +++ b/src/Data/List/Relation/Unary/All.agda @@ -234,17 +234,3 @@ decide p∪q (x ∷ xs) with p∪q x search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs search P? = decide (Sum.swap ∘ Dec.toSum ∘ P?) - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.4 - -all = all? -{-# WARNING_ON_USAGE all -"Warning: all was deprecated in v1.4. -Please use all? instead." -#-} diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda index 820860fb4a..6e60adda3e 100644 --- a/src/Data/List/Relation/Unary/All/Properties.agda +++ b/src/Data/List/Relation/Unary/All/Properties.agda @@ -705,14 +705,6 @@ module _ (S : Setoid c ℓ) where -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 1.3 - -Any¬→¬All = Any¬⇒¬All -{-# WARNING_ON_USAGE Any¬→¬All -"Warning: Any¬→¬All was deprecated in v1.3. -Please use Any¬⇒¬All instead." -#-} - -- Version 2.0 updateAt-id-relative = updateAt-id-local diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda index 8148ced7bc..0187d4ceeb 100644 --- a/src/Data/List/Relation/Unary/Any.agda +++ b/src/Data/List/Relation/Unary/Any.agda @@ -92,18 +92,3 @@ any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs) satisfiable : Satisfiable P → Satisfiable (Any P) satisfiable (x , Px) = [ x ] , here Px - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.4 - -any = any? -{-# WARNING_ON_USAGE any -"Warning: any was deprecated in v1.4. -Please use any? instead." -#-} diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 0aca3a757c..1970f878b9 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -1507,34 +1507,6 @@ pred[x]+y≡x+pred[y] {x} {y} x≢0 y≢0 = begin -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 1.4 - -*-+-isSemiringWithoutAnnihilatingZero = +-*-isSemiringWithoutAnnihilatingZero -{-# WARNING_ON_USAGE *-+-isSemiringWithoutAnnihilatingZero -"Warning: *-+-isSemiringWithoutAnnihilatingZero was deprecated in v1.4. -Please use +-*-isSemiringWithoutAnnihilatingZero instead." -#-} -*-+-isSemiring = +-*-isSemiring -{-# WARNING_ON_USAGE *-+-isSemiring -"Warning: *-+-isSemiring was deprecated in v1.4. -Please use +-*-isSemiring instead." -#-} -*-+-isCommutativeSemiring = +-*-isCommutativeSemiring -{-# WARNING_ON_USAGE *-+-isCommutativeSemiring -"Warning: *-+-isCommutativeSemiring was deprecated in v1.4. -Please use +-*-isCommutativeSemiring instead." -#-} -*-+-semiring = +-*-semiring -{-# WARNING_ON_USAGE *-+-semiring -"Warning: *-+-semiring was deprecated in v1.4. -Please use +-*-semiring instead." -#-} -*-+-commutativeSemiring = +-*-commutativeSemiring -{-# WARNING_ON_USAGE *-+-commutativeSemiring -"Warning: *-+-commutativeSemiring was deprecated in v1.4. -Please use +-*-commutativeSemiring instead." -#-} - -- Version 2.0 {- issue1858/issue1755: raw bundles have moved to `Data.X.Base` -} diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 6286cd3d7d..9f7c7990ec 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -48,6 +48,7 @@ open import Relation.Binary.Consequences open import Relation.Binary.PropositionalEquality open import Relation.Binary.Structures open import Relation.Binary.Structures.Biased +open import Relation.Binary.Morphism.Construct.PropositionalEquality open import Relation.Nullary.Decidable using (True; via-injection; map′; recompute; no; yes; Dec; _because_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) @@ -1083,15 +1084,15 @@ m?_) - ------------------------------------------------------------------------- --- Deprecated - --- Version 1.0 - -open import Data.Rational.Properties public - using (drop-*≤*; ≃⇒≡; ≡⇒≃) - --- Version 1.5 - -import Data.Integer.Show as ℤ -open import Data.String.Base using (String; _++_) - -show : ℚ → String -show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p) - -{-# WARNING_ON_USAGE show -"Warning: show was deprecated in v1.5. -Please use Data.Rational.Show's show instead." -#-} diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 55f72423be..d8313d985d 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1945,14 +1945,6 @@ pos⊔pos⇒pos p q = positive (⊔-mono-< (positive⁻¹ p) (positive⁻¹ q)) -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 1.5 - -neg-mono-<-> = neg-mono-< -{-# WARNING_ON_USAGE neg-mono-<-> -"Warning: neg-mono-<-> was deprecated in v1.5. -Please use neg-mono-< instead." -#-} - -- Version 2.0 ↥[p/q]≡p = ↥[n/d]≡n diff --git a/src/Data/Record.agda b/src/Data/Record.agda index 778014e5c2..edb0839e2c 100644 --- a/src/Data/Record.agda +++ b/src/Data/Record.agda @@ -62,6 +62,7 @@ mutual -- Record is a record type to ensure that the signature can be -- inferred from a value of type Record Sig. + {-# ETA_EQUALITY #-} -- Lie to get std-lib building record Record {s} (Sig : Signature s) : Set s where eta-equality inductive diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda index 7e4228ea87..900e457c7e 100644 --- a/src/Data/Vec/Relation/Unary/All.agda +++ b/src/Data/Vec/Relation/Unary/All.agda @@ -131,10 +131,3 @@ decide p∪q [] = inj₁ [] decide p∪q (x ∷ xs) with p∪q x ... | inj₂ qx = inj₂ (here qx) ... | inj₁ px = Sum.map (px ∷_) there (decide p∪q xs) - - -all = all? -{-# WARNING_ON_USAGE all -"Warning: all was deprecated in v1.4. -Please use all? instead." -#-} diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index b23e11387e..5679ea5662 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -80,9 +80,3 @@ any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs) satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n}) satisfiable (x , p) {zero} = x ∷ [] , here p satisfiable (x , p) {suc n} = Product.map (x ∷_) there (satisfiable (x , p)) - -any = any? -{-# WARNING_ON_USAGE any -"Warning: any was deprecated in v1.4. -Please use any? instead." -#-} diff --git a/src/Function/Base.agda b/src/Function/Base.agda index b3741f1390..3cb8b86ca0 100644 --- a/src/Function/Base.agda +++ b/src/Function/Base.agda @@ -256,14 +256,6 @@ _*_ on f = f -⟨ _*_ ⟩- f -- Please use the new names as continuing support for the old names is -- not guaranteed. --- Version 1.4 - -_-[_]-_ = _-⟪_⟫-_ -{-# WARNING_ON_USAGE _-[_]-_ -"Warning: Function._-[_]-_ was deprecated in v1.4. -Please use _-⟪_⟫-_ instead." -#-} - -- Version 2.0 case_return_of_ = case_returning_of_ diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index 4d5aec6a74..dfd19d1b22 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -151,118 +151,3 @@ module Subrelation {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂} wellFounded : WellFounded _<₂_ → WellFounded _<₁_ wellFounded wf = λ x → accessible (wf x) - - --- DEPRECATED in v1.4. --- Please use proofs in `Relation.Binary.Construct.On` instead. -module InverseImage {_<_ : Rel B ℓ} (f : A → B) where - - accessible : ∀ {x} → Acc _<_ (f x) → Acc (_<_ on f) x - accessible (acc rs) = acc λ fy>=_; _>>_) - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - -import Reflection.AST.Abstraction as Abstraction -import Reflection.AST.Argument as Argument -import Reflection.AST.Definition as Definition -import Reflection.AST.Meta as Meta -import Reflection.AST.Name as Name -import Reflection.AST.Literal as Literal -import Reflection.AST.Pattern as Pattern -import Reflection.AST.Term as Term -import Reflection.AST.Argument.Modality as Modality -import Reflection.AST.Argument.Quantity as Quantity -import Reflection.AST.Argument.Relevance as Relevance -import Reflection.AST.Argument.Visibility as Visibility -import Reflection.AST.Argument.Information as Information - --- Version 1.3 - -Arg-info = Information.ArgInfo -{-# WARNING_ON_USAGE Arg-info -"Warning: Arg-info was deprecated in v1.3. -Please use Reflection.AST.Argument.Information's ArgInfo instead." -#-} - -infix 4 _≟-Lit_ _≟-Name_ _≟-Meta_ _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_ - _≟-Pattern_ _≟-ArgPatterns_ - -_≟-Lit_ = Literal._≡?_ -{-# WARNING_ON_USAGE _≟-Lit_ -"Warning: _≟-Lit_ was deprecated in v1.3. -Please use Reflection.AST.Literal's _≡?_ instead." -#-} - -_≟-Name_ = Name._≡?_ -{-# WARNING_ON_USAGE _≟-Name_ -"Warning: _≟-Name_ was deprecated in v1.3. -Please use Reflection.AST.Name's _≡?_ instead." -#-} - -_≟-Meta_ = Meta._≡?_ -{-# WARNING_ON_USAGE _≟-Meta_ -"Warning: _≟-Meta_ was deprecated in v1.3. -Please use Reflection.AST.Meta's _≡?_ instead." -#-} - -_≟-Visibility_ = Visibility._≡?_ -{-# WARNING_ON_USAGE _≟-Visibility_ -"Warning: _≟-Visibility_ was deprecated in v1.3. -Please use Reflection.AST.Argument.Visibility's _≡?_ instead." -#-} - -_≟-Relevance_ = Relevance._≡?_ -{-# WARNING_ON_USAGE _≟-Relevance_ -"Warning: _≟-Relevance_ was deprecated in v1.3. -Please use Reflection.AST.Argument.Relevance's _≡?_ instead." -#-} - -_≟-Arg-info_ = Information._≡?_ -{-# WARNING_ON_USAGE _≟-Arg-info_ -"Warning: _≟-Arg-info_ was deprecated in v1.3. -Please use Reflection.AST.Argument.Information's _≡?_ instead." -#-} - -_≟-Pattern_ = Pattern._≡?_ -{-# WARNING_ON_USAGE _≟-Pattern_ -"Warning: _≟-Pattern_ was deprecated in v1.3. -Please use Reflection.AST.Pattern's _≡?_ instead." -#-} - -_≟-ArgPatterns_ = Pattern._≟s_ -{-# WARNING_ON_USAGE _≟-ArgPatterns_ -"Warning: _≟-ArgPatterns_ was deprecated in v1.3. -Please use Reflection.AST.Pattern's _≟s_ instead." -#-} - -map-Abs = Abstraction.map -{-# WARNING_ON_USAGE map-Abs -"Warning: map-Abs was deprecated in v1.3. -Please use Reflection.AST.Abstraction's map instead." -#-} - -map-Arg = Argument.map -{-# WARNING_ON_USAGE map-Arg -"Warning: map-Arg was deprecated in v1.3. -Please use Reflection.AST.Argument's map instead." -#-} - -map-Args = Argument.map-Args -{-# WARNING_ON_USAGE map-Args -"Warning: map-Args was deprecated in v1.3. -Please use Reflection.AST.Argument's map-Args instead." -#-} - -visibility = Information.visibility -{-# WARNING_ON_USAGE visibility -"Warning: visibility was deprecated in v1.3. -Please use Reflection.AST.Argument.Information's visibility instead." -#-} - -relevance = Modality.relevance -{-# WARNING_ON_USAGE relevance -"Warning: relevance was deprecated in v1.3. -Please use Reflection.AST.Argument.Modality's relevance instead." -#-} - -infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ - _≟-Clause_ _≟-Clauses_ _≟_ - _≟-Sort_ - -_≟-AbsTerm_ = Term._≡?-AbsTerm_ -{-# WARNING_ON_USAGE _≟-AbsTerm_ -"Warning: _≟-AbsTerm_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-AbsTerm_ instead." -#-} - -_≟-AbsType_ = Term._≡?-AbsType_ -{-# WARNING_ON_USAGE _≟-AbsType_ -"Warning: _≟-AbsType_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-AbsType_ instead." -#-} - -_≟-ArgTerm_ = Term._≡?-ArgTerm_ -{-# WARNING_ON_USAGE _≟-ArgTerm_ -"Warning: _≟-ArgTerm_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-ArgTerm_ instead." -#-} - -_≟-ArgType_ = Term._≡?-ArgType_ -{-# WARNING_ON_USAGE _≟-ArgType_ -"Warning: _≟-ArgType_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-ArgType_ instead." -#-} - -_≟-Args_ = Term._≡?-Args_ -{-# WARNING_ON_USAGE _≟-Args_ -"Warning: _≟-Args_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-Args_ instead." -#-} - -_≟-Clause_ = Term._≡?-Clause_ -{-# WARNING_ON_USAGE _≟-Clause_ -"Warning: _≟-Clause_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-Clause_ instead." -#-} - -_≟-Clauses_ = Term._≡?-Clauses_ -{-# WARNING_ON_USAGE _≟-Clauses_ -"Warning: _≟-Clauses_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-Clauses_ instead." -#-} - -_≟_ = Term._≡?_ -{-# WARNING_ON_USAGE _≟_ -"Warning: _≟_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?_ instead." -#-} - -_≟-Sort_ = Term._≡?-Sort_ -{-# WARNING_ON_USAGE _≟-Sort_ -"Warning: _≟-Sort_ was deprecated in v1.3. -Please use Reflection.AST.Term's _≡?-Sort_ instead." -#-} diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 66ca609dc6..9d1ff33219 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -372,16 +372,6 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh open DecStrictPartialOrder decStrictPartialOrder public using (module Eq) - decSetoid : DecSetoid c ℓ₁ - decSetoid = record - { isDecEquivalence = Eq.isDecEquivalence - } - {-# WARNING_ON_USAGE decSetoid - "Warning: decSetoid was deprecated in v1.3. - Please use Eq.decSetoid instead." - #-} - - record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ field diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda index 3e2dc284d3..a860a87a60 100644 --- a/src/Relation/Binary/Consequences.agda +++ b/src/Relation/Binary/Consequences.agda @@ -220,109 +220,3 @@ module _ {R : REL A B ℓ₁} {S : REL B A ℓ₂} where flip-Connex : Connex R S → Connex S R flip-Connex f x y = Sum.swap (f y x) - - - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.6 - -subst⟶respˡ = subst⇒respˡ -{-# WARNING_ON_USAGE subst⟶respˡ -"Warning: subst⟶respˡ was deprecated in v1.6. -Please use subst⇒respˡ instead." -#-} -subst⟶respʳ = subst⇒respʳ -{-# WARNING_ON_USAGE subst⟶respʳ -"Warning: subst⟶respʳ was deprecated in v1.6. -Please use subst⇒respʳ instead." -#-} -subst⟶resp₂ = subst⇒resp₂ -{-# WARNING_ON_USAGE subst⟶resp₂ -"Warning: subst⟶resp₂ was deprecated in v1.6. -Please use subst⇒resp₂ instead." -#-} -P-resp⟶¬P-resp = resp⇒¬-resp -{-# WARNING_ON_USAGE P-resp⟶¬P-resp -"Warning: P-resp⟶¬P-resp was deprecated in v1.6. -Please use resp⇒¬-resp instead." -#-} -total⟶refl = total⇒refl -{-# WARNING_ON_USAGE total⟶refl -"Warning: total⟶refl was deprecated in v1.6. -Please use total⇒refl instead." -#-} -total+dec⟶dec = total∧dec⇒dec -{-# WARNING_ON_USAGE total+dec⟶dec -"Warning: total+dec⟶dec was deprecated in v1.6. -Please use total∧dec⇒dec instead." -#-} -trans∧irr⟶asym = trans∧irr⇒asym -{-# WARNING_ON_USAGE trans∧irr⟶asym -"Warning: trans∧irr⟶asym was deprecated in v1.6. -Please use trans∧irr⇒asym instead." -#-} -irr∧antisym⟶asym = irr∧antisym⇒asym -{-# WARNING_ON_USAGE irr∧antisym⟶asym -"Warning: irr∧antisym⟶asym was deprecated in v1.6. -Please use irr∧antisym⇒asym instead." -#-} -asym⟶antisym = asym⇒antisym -{-# WARNING_ON_USAGE asym⟶antisym -"Warning: asym⟶antisym was deprecated in v1.6. -Please use asym⇒antisym instead." -#-} -asym⟶irr = asym⇒irr -{-# WARNING_ON_USAGE asym⟶irr -"Warning: asym⟶irr was deprecated in v1.6. -Please use asym⇒irr instead." -#-} -tri⟶asym = tri⇒asym -{-# WARNING_ON_USAGE tri⟶asym -"Warning: tri⟶asym was deprecated in v1.6. -Please use tri⇒asym instead." -#-} -tri⟶irr = tri⇒irr -{-# WARNING_ON_USAGE tri⟶irr -"Warning: tri⟶irr was deprecated in v1.6. -Please use tri⇒irr instead." -#-} -tri⟶dec≈ = tri⇒dec≈ -{-# WARNING_ON_USAGE tri⟶dec≈ -"Warning: tri⟶dec≈ was deprecated in v1.6. -Please use tri⇒dec≈ instead." -#-} -tri⟶dec< = tri⇒dec< -{-# WARNING_ON_USAGE tri⟶dec< -"Warning: tri⟶dec< was deprecated in v1.6. -Please use tri⇒dec< instead." -#-} -trans∧tri⟶respʳ≈ = trans∧tri⇒respʳ -{-# WARNING_ON_USAGE trans∧tri⟶respʳ≈ -"Warning: trans∧tri⟶respʳ≈ was deprecated in v1.6. -Please use trans∧tri⇒respʳ instead." -#-} -trans∧tri⟶respˡ≈ = trans∧tri⇒respˡ -{-# WARNING_ON_USAGE trans∧tri⟶respˡ≈ -"Warning: trans∧tri⟶respˡ≈ was deprecated in v1.6. -Please use trans∧tri⇒respˡ instead." -#-} -trans∧tri⟶resp≈ = trans∧tri⇒resp -{-# WARNING_ON_USAGE trans∧tri⟶resp≈ -"Warning: trans∧tri⟶resp≈ was deprecated in v1.6. -Please use trans∧tri⇒resp instead." -#-} -dec⟶weaklyDec = dec⇒weaklyDec -{-# WARNING_ON_USAGE dec⟶weaklyDec -"Warning: dec⟶weaklyDec was deprecated in v1.6. -Please use dec⇒weaklyDec instead." -#-} -dec⟶recomputable = dec⇒recomputable -{-# WARNING_ON_USAGE dec⟶recomputable -"Warning: dec⟶recomputable was deprecated in v1.6. -Please use dec⇒recomputable instead." -#-} diff --git a/src/Relation/Binary/Construct/Closure/Reflexive.agda b/src/Relation/Binary/Construct/Closure/Reflexive.agda index 2a509fe985..3e8a4f4c96 100644 --- a/src/Relation/Binary/Construct/Closure/Reflexive.agda +++ b/src/Relation/Binary/Construct/Closure/Reflexive.agda @@ -64,19 +64,3 @@ private just : A → Maybe A just = [_] - - - ------------------------------------------------------------------------- --- Deprecations ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- v1.5 - -Refl = ReflClosure -{-# WARNING_ON_USAGE Refl -"Warning: Refl was deprecated in v1.5. -Please use ReflClosure instead." -#-} diff --git a/src/Relation/Binary/Construct/Closure/Transitive.agda b/src/Relation/Binary/Construct/Closure/Transitive.agda index a2b3214c85..f021470d2c 100644 --- a/src/Relation/Binary/Construct/Closure/Transitive.agda +++ b/src/Relation/Binary/Construct/Closure/Transitive.agda @@ -146,17 +146,3 @@ equivalent {_∼_ = _∼_} = mk⇔ complete sound sound : TransClosure _∼_ ⇒ Plus _∼_ sound [ x∼y ] = [ x∼y ] sound (x∼y ∷ y∼⁺z) = _ ∼⁺⟨ [ x∼y ] ⟩ sound y∼⁺z - ------------------------------------------------------------------------- --- Deprecations ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- v1.5 - -Plus′ = TransClosure -{-# WARNING_ON_USAGE Plus′ -"Warning: Plus′ was deprecated in v1.5. -Please use TransClosure instead." -#-} diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda index b8b3f13067..a6dd451b2f 100644 --- a/src/Relation/Binary/Construct/StrictToNonStrict.agda +++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda @@ -149,19 +149,3 @@ isDecTotalOrder STO = record ; _≤?_ = decidable′ S.compare } where module S = IsStrictTotalOrder STO - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.4 - -decidable' : Trichotomous _≈_ _<_ → Decidable _≤_ -decidable' = decidable′ -{-# WARNING_ON_USAGE decidable' -"Warning: decidable' (ending in an apostrophe) was deprecated in v1.4. -Please use decidable′ (ending in a prime) instead." -#-} diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda index 832b3c3f6f..b39529bb32 100644 --- a/src/Relation/Binary/Reasoning/Base/Partial.agda +++ b/src/Relation/Binary/Reasoning/Base/Partial.agda @@ -70,21 +70,3 @@ open begin-subrelation-syntax _IsRelatedTo_ relToSubRelation public open ≡-syntax _IsRelatedTo_ ≡-go public open ∼-syntax _IsRelatedTo_ _IsRelatedTo_ ∼-go public open end-syntax _IsRelatedTo_ stop public - ------------------------------------------------------------------------- --- DEPRECATED NAMES ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 1.6 - -infix 3 _∎⟨_⟩ - -_∎⟨_⟩ : ∀ x → x ∼ x → x IsRelatedTo x -_ ∎⟨ x∼x ⟩ = relTo x∼x -{-# WARNING_ON_USAGE _∎⟨_⟩ -"Warning: _∎⟨_⟩ was deprecated in v1.6. -Please use _∎ instead if used in a chain, otherwise simply provide -the proof of reflexivity directly without using these combinators." -#-} diff --git a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda index 825ac21f6d..e12bfe1be5 100644 --- a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda +++ b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda @@ -94,7 +94,7 @@ record _-Raw-AlmostCommutative⟶_ module T = AlmostCommutativeRing To open Morphism.Definitions F.Carrier T.Carrier T._≈_ field - ⟦_⟧ : Morphism + ⟦_⟧ : F.Carrier → T.Carrier +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_ *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_ -‿homo : Homomorphic₁ ⟦_⟧ (F.-_) (T.-_) From fb850ce0deab6a9e4fecf109c9344e96736d9b21 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 25 Jun 2026 09:58:31 -0400 Subject: [PATCH 06/22] =?UTF-8?q?Revert=20removal=20of=20=5F=E2=89=88=3F?= =?UTF-8?q?=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Char.agda | 2 +- src/Data/Char/Properties.agda | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Data/Char.agda b/src/Data/Char.agda index 98781dac13..ecca28afa8 100644 --- a/src/Data/Char.agda +++ b/src/Data/Char.agda @@ -13,4 +13,4 @@ module Data.Char where open import Data.Char.Base public open import Data.Char.Properties - using (_≟_; _≡?_; _ Date: Thu, 25 Jun 2026 09:59:27 -0400 Subject: [PATCH 07/22] =?UTF-8?q?Replace=20export=20of=20=5F=3D=3D=5F=20wi?= =?UTF-8?q?th=20=5F=E2=89=A1=E1=B5=87=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Char.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Char.agda b/src/Data/Char.agda index ecca28afa8..deaf36f167 100644 --- a/src/Data/Char.agda +++ b/src/Data/Char.agda @@ -13,4 +13,4 @@ module Data.Char where open import Data.Char.Base public open import Data.Char.Properties - using (_≈?_;_≟_; _≡?_; _ Date: Thu, 25 Jun 2026 10:09:42 -0400 Subject: [PATCH 08/22] Revert ETA_EQUALITY pragma lie --- src/Data/Record.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Record.agda b/src/Data/Record.agda index edb0839e2c..778014e5c2 100644 --- a/src/Data/Record.agda +++ b/src/Data/Record.agda @@ -62,7 +62,6 @@ mutual -- Record is a record type to ensure that the signature can be -- inferred from a value of type Record Sig. - {-# ETA_EQUALITY #-} -- Lie to get std-lib building record Record {s} (Sig : Signature s) : Set s where eta-equality inductive From 98bd0bd0add62650088b6f73545556d92244acf0 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 25 Jun 2026 10:19:29 -0400 Subject: [PATCH 09/22] Revert removal of v2.4 deprecation and fix warning to state v2.4 instead of v1.4 --- .../List/Fresh/Membership/Setoid/Properties.agda | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda index 95817d9c7d..4ffa1b0c25 100644 --- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda +++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda @@ -158,3 +158,17 @@ All[x≉]-∉ : All (x ≉_) xs → x ∉ xs All[x≉]-∉ [] () All[x≉]-∉ (p ∷ ps) (here x≈y) = p x≈y All[x≉]-∉ (p ∷ ps) (there x∈ys) = All[x≉]-∉ ps x∈ys + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +≈-subst-∈ = ∈-resp-≈ +{-# WARNING_ON_USAGE ≈-subst-∈ +"Warning: ≈-subst-∈ was deprecated in v2.4. +Please use ∈-resp-≈ instead." +#-} From 8325d439a16c7ddea99dc9c11ea4d8ef7a8207fd Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Thu, 25 Jun 2026 10:21:37 -0400 Subject: [PATCH 10/22] Inline congruence proof Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --- src/Data/Nat/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 9f7c7990ec..b52cf4a3c1 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1086,7 +1086,7 @@ m Date: Thu, 25 Jun 2026 10:28:06 -0400 Subject: [PATCH 11/22] Remove unneeded module --- src/Data/Nat/Properties.agda | 1 - .../Construct/PropositionalEquality.agda | 16 ---------------- 2 files changed, 17 deletions(-) delete mode 100644 src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index b52cf4a3c1..2072103418 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -48,7 +48,6 @@ open import Relation.Binary.Consequences open import Relation.Binary.PropositionalEquality open import Relation.Binary.Structures open import Relation.Binary.Structures.Biased -open import Relation.Binary.Morphism.Construct.PropositionalEquality open import Relation.Nullary.Decidable using (True; via-injection; map′; recompute; no; yes; Dec; _because_) open import Relation.Nullary.Negation.Core using (¬_; contradiction) diff --git a/src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda b/src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda deleted file mode 100644 index fdeaff2bd7..0000000000 --- a/src/Relation/Binary/Morphism/Construct/PropositionalEquality.agda +++ /dev/null @@ -1,16 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- Propositional Equality Lemmas over Morphisms ------------------------------------------------------------------------- - -{-# OPTIONS --without-K --safe #-} - -open import Agda.Builtin.Equality using (_≡_) -open import Relation.Binary.PropositionalEquality.Core using (cong) -open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism) - -module Relation.Binary.Morphism.Construct.PropositionalEquality where - -cong-IsRelHomomorphism : ∀ {a b} {A : Set a} {B : Set b} → (f : A → B) → IsRelHomomorphism _≡_ _≡_ f -cong-IsRelHomomorphism f .IsRelHomomorphism.cong = cong f From 5424d58efc0ead20084d0591d4b466026d7802c3 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 25 Jun 2026 10:29:38 -0400 Subject: [PATCH 12/22] Remove comment --- src/Data/Nat/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 2072103418..26d4e3d1c7 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1083,7 +1083,7 @@ m Date: Thu, 25 Jun 2026 10:32:15 -0400 Subject: [PATCH 13/22] Revert "Remove useless pattern attribute" This reverts commit 07f12b7ed43c2fdc3fa102bfd6837ca568a509c7. --- src/Reflection/AST/Traversal.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Reflection/AST/Traversal.agda b/src/Reflection/AST/Traversal.agda index c99965800d..e2a96b4bc2 100644 --- a/src/Reflection/AST/Traversal.agda +++ b/src/Reflection/AST/Traversal.agda @@ -27,6 +27,7 @@ open RawApplicative AppF -- compute the length of the context everytime it's needed. record Cxt : Set where constructor _,_ + pattern field len : ℕ context : List (String × Arg Term) From ec316d1911e9a8035465631ab80d0ce3d5f80148 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 25 Jun 2026 12:04:17 -0400 Subject: [PATCH 14/22] Remove now unneeded warning suppression --- src/Data/List.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/List.agda b/src/Data/List.agda index 98b2aa6e37..68d1d610ae 100644 --- a/src/Data/List.agda +++ b/src/Data/List.agda @@ -8,7 +8,6 @@ -- lists. {-# OPTIONS --without-K --safe #-} -{-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans module Data.List where From 4742567ded140f69f5afd7277c9e577f84ab1ef5 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Mon, 29 Jun 2026 10:17:29 -0400 Subject: [PATCH 15/22] Add whitespace for consistent formatting Co-authored-by: Jacques Carette --- src/Data/Char.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Char.agda b/src/Data/Char.agda index deaf36f167..7bec55d8ca 100644 --- a/src/Data/Char.agda +++ b/src/Data/Char.agda @@ -13,4 +13,4 @@ module Data.Char where open import Data.Char.Base public open import Data.Char.Properties - using (_≈?_;_≟_; _≡?_; _ Date: Mon, 29 Jun 2026 10:22:00 -0400 Subject: [PATCH 16/22] Export _==_ --- src/Data/Char.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Char.agda b/src/Data/Char.agda index 7bec55d8ca..3e31fe5ef2 100644 --- a/src/Data/Char.agda +++ b/src/Data/Char.agda @@ -13,4 +13,4 @@ module Data.Char where open import Data.Char.Base public open import Data.Char.Properties - using (_≈?_; _≟_; _≡?_; _ Date: Mon, 29 Jun 2026 10:27:55 -0400 Subject: [PATCH 17/22] Remove ^-isSemigroupMorphism and ^-isMonoidMorphism --- src/Function/Endomorphism/Setoid.agda | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/src/Function/Endomorphism/Setoid.agda b/src/Function/Endomorphism/Setoid.agda index a357997075..f5fa5908d9 100644 --- a/src/Function/Endomorphism/Setoid.agda +++ b/src/Function/Endomorphism/Setoid.agda @@ -80,18 +80,3 @@ f ^ suc n = f ∘ (f ^ n) ∘-id-monoid : Monoid _ _ ∘-id-monoid = record { isMonoid = ∘-id-isMonoid } - ------------------------------------------------------------------------- --- Homomorphism - -^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_) -^-isSemigroupMorphism f = record - { ⟦⟧-cong = ^-cong₂ f - ; ∙-homo = ^-homo f - } - -^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_) -^-isMonoidMorphism f = record - { sm-homo = ^-isSemigroupMorphism f - ; ε-homo = λ x≈y → x≈y - } From 55920f7fa1a0d82815c6619521f3fd7338304a4d Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 29 Jun 2026 10:44:15 -0400 Subject: [PATCH 18/22] Update CHANGELOG to mention removal of 1.x deprecations --- CHANGELOG.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4e4067ff37..4afe574a39 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,6 +20,32 @@ Highlights The change leads to a number of (trivial) renamings/deprecations, others more substantive in `Data.{Nat|Fin}.Properties` for the concrete datatypes, which are summarised below, but are not each documented for all affected modules. + +* Any v1.x deprecation has been removed entirely. + This involves the removal of modules: + - `Algebra.FunctionProperties.Consequences.Core` + - `Algebra.FunctionProperties.Consequences.Propositional` + - `Algebra.FunctionProperties.Consequences` + - `Algebra.Operations.CommutativeMonoid` + - `Algebra.Operations.Ring` + - `Algebra.Operations.Semiring` + - `Data.AVL.Indexed.WithK` + - `Data.AVL.NonEmpty.Propositional` + - `Data.AVL.Height` + - `Data.AVL.Indexed` + - `Data.AVL.IndexedMap` + - `Data.AVL.Key` + - `Data.AVL.Map` + - `Data.AVL.NonEmpty` + - `Data.AVL.Value` + - `Data.AVL` + - `Foreign.Haskell.Maybe` + - `Relation.Binary.OrderMorphism` + - `Text.Tree.Linear` + - `Strict` + Several Definitions from other modules have also been removed. + +* `^-isSemigroupMorphism` and `^-isMonoidMorphism` from `Function.Endomorphism.Setoid` has been removed Bug-fixes --------- @@ -60,6 +86,8 @@ Non-backwards compatible changes Data.Tree.Rose.Properties Data.Tree.Rose.Show ``` + +* `^-semigroup-morphism` and `^-monoid-morphism` in `Data.Nat.Properties` have had their definitions and signatures updated to use `IsMagmaHomomorphism` and `IsMonoidHomomorphism` respectively, inline with the removal of 1.x deprecations. Minor improvements ------------------ From 72a146755b93c9bb3a544e427a690395ed11e3aa Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 29 Jun 2026 10:45:38 -0400 Subject: [PATCH 19/22] Add newline --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4afe574a39..e5a8849c72 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -43,6 +43,7 @@ Highlights - `Relation.Binary.OrderMorphism` - `Text.Tree.Linear` - `Strict` + Several Definitions from other modules have also been removed. * `^-isSemigroupMorphism` and `^-isMonoidMorphism` from `Function.Endomorphism.Setoid` has been removed From 82656d3ae0c9f3ec5896546dfdf40460f21bed3a Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Mon, 29 Jun 2026 16:09:10 -0400 Subject: [PATCH 20/22] Fix whitespace and grammar --- CHANGELOG.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e5a8849c72..fc94db2ddc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -20,7 +20,7 @@ Highlights The change leads to a number of (trivial) renamings/deprecations, others more substantive in `Data.{Nat|Fin}.Properties` for the concrete datatypes, which are summarised below, but are not each documented for all affected modules. - + * Any v1.x deprecation has been removed entirely. This involves the removal of modules: - `Algebra.FunctionProperties.Consequences.Core` @@ -43,10 +43,10 @@ Highlights - `Relation.Binary.OrderMorphism` - `Text.Tree.Linear` - `Strict` - + Several Definitions from other modules have also been removed. -* `^-isSemigroupMorphism` and `^-isMonoidMorphism` from `Function.Endomorphism.Setoid` has been removed +* `^-isSemigroupMorphism` and `^-isMonoidMorphism` from `Function.Endomorphism.Setoid` have been removed Bug-fixes --------- @@ -87,7 +87,7 @@ Non-backwards compatible changes Data.Tree.Rose.Properties Data.Tree.Rose.Show ``` - + * `^-semigroup-morphism` and `^-monoid-morphism` in `Data.Nat.Properties` have had their definitions and signatures updated to use `IsMagmaHomomorphism` and `IsMonoidHomomorphism` respectively, inline with the removal of 1.x deprecations. Minor improvements From 34cda4feb2e002305beb9a06e94f8a2e7272eafc Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Mon, 29 Jun 2026 18:50:11 -0400 Subject: [PATCH 21/22] Remove ^-isSemigroupMorphism and ^-isMonoidMorphism --- src/Function/Endomorphism/Propositional.agda | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda index c6b49c4877..d09b8135e1 100644 --- a/src/Function/Endomorphism/Propositional.agda +++ b/src/Function/Endomorphism/Propositional.agda @@ -84,18 +84,3 @@ f ^ suc n = f ∘′ (f ^ n) ∘-id-monoid : Monoid _ _ ∘-id-monoid = record { isMonoid = ∘-id-isMonoid } - ------------------------------------------------------------------------- --- Homomorphism - -^-isSemigroupMorphism : ∀ f → IsSemigroupMorphism +-semigroup ∘-semigroup (f ^_) -^-isSemigroupMorphism f = record - { ⟦⟧-cong = cong (f ^_) - ; ∙-homo = ^-homo f - } - -^-isMonoidMorphism : ∀ f → IsMonoidMorphism +-0-monoid ∘-id-monoid (f ^_) -^-isMonoidMorphism f = record - { sm-homo = ^-isSemigroupMorphism f - ; ε-homo = refl - } From 6cab81700d3a47bbcfc1b57bd0a9d949b81c06c5 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Mon, 29 Jun 2026 18:52:31 -0400 Subject: [PATCH 22/22] Update CHANGELOG.md --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fc94db2ddc..bc0d0149bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -46,7 +46,7 @@ Highlights Several Definitions from other modules have also been removed. -* `^-isSemigroupMorphism` and `^-isMonoidMorphism` from `Function.Endomorphism.Setoid` have been removed +* `^-isSemigroupMorphism` and `^-isMonoidMorphism` from both `Function.Endomorphism.Setoid` and `Function.Endomorphism.Propositional` have been removed Bug-fixes ---------