Removed all deprecated elements up to v1.2 (#1715)

Author: MatthewDaggitt

CHANGELOG.md

@@ -48,7 +48,7 @@ Non-backwards compatible changes
 
 #### Removed deprecated names
 
-* All modules and names that were deprecated prior to v1.0 have been removed.
+* All modules and names that were deprecated in v1.2 and before have been removed.
 
 #### Moved `Codata` modules to `Codata.Sized`
 
@@ -596,6 +596,9 @@ Deprecated names
   *-monoˡ-≤-neg    ↦  *-monoˡ-≤-nonPos
   *-cancelˡ-<-neg  ↦  *-cancelˡ-<-nonPos
   *-cancelʳ-<-neg  ↦  *-cancelʳ-<-nonPos
+  
+  ^-semigroup-morphism ↦ ^-isMagmaHomomorphism
+  ^-monoid-morphism    ↦ ^-isMonoidHomomorphism
   ```
 
 * In `Data.List.Properties`:
@@ -679,13 +682,6 @@ Deprecated names
   id-↔   ↦   ↔-id
   ```
 
-* Factorial, combinations and permutations for ℕ.
-  ```
-  Data.Nat.Combinatorics
-  Data.Nat.Combinatorics.Base
-  Data.Nat.Combinatorics.Spec
-  ```
-
 * In `Function.Construct.Symmetry`:
   ```
   sym-⤖   ↦   ⤖-sym
@@ -701,6 +697,11 @@ Deprecated names
   fromForeign ↦ Foreign.Haskell.Coerce.coerce
   ```
 
+* In `Relation.Binary.Properties.Preorder`:
+  ```
+  invIsPreorder ↦ converse-isPreorder
+  invPreorder   ↦ converse-preorder
+  ```
 
 New modules
 -----------
@@ -748,6 +749,13 @@ New modules
   Data.List.Fresh.NonEmpty
   ```
 
+* Combinations and permutations for ℕ.
+  ```
+  Data.Nat.Combinatorics
+  Data.Nat.Combinatorics.Base
+  Data.Nat.Combinatorics.Spec
+  ```
+
 * Reflection utilities for some specific types:
   ```
   Data.List.Reflection
@@ -1015,8 +1023,11 @@ Other minor changes
   ^-*-assoc      : (i ^ m) ^ n ≡ i ^ (m ℕ.* n)
   ^-distribˡ-+-* : i ^ (m ℕ.+ n) ≡ i ^ m * i ^ n
 
-  ^-semigroup-morphism : IsSemigroupMorphism ℕ.+-semigroup *-semigroup (i ^_)
-  ^-monoid-morphism    : IsMonoidMorphism ℕ.+-0-monoid *-1-monoid (i ^_)
+  *-rawMagma    : RawMagma 0ℓ 0ℓ
+  *-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+
+  ^-isMagmaHomomorphism  : IsMagmaHomomorphism  ℕ.+-rawMagma    *-rawMagma    (i ^_)
+  ^-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid *-1-rawMonoid (i ^_)
   ```
 
 * Added new functions in `Data.List`:
@@ -1690,4 +1701,4 @@ This is a full list of proofs that have changed form to use irrelevant instance
   ```agda
   iterate : (A → A) → A → ℕ → A
   iterate-is-fold : ∀ (z : A) s m → fold z s m ≡ iterate s z m
-  ```
+  ```

GNUmakefile

@@ -1,6 +1,7 @@
 AGDA_EXEC ?= agda
-RTS_OPTIONS=+RTS -M4.0G -H3.5G -A128M -RTS
-AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)
+AGDA_OPTIONS=-Werror
+AGDA_RTS_OPTIONS=+RTS -M4.0G -H3.5G -A128M -RTS
+AGDA=$(AGDA_EXEC) $(AGDA_OPTIONS) $(AGDA_RTS_OPTIONS)
 
 # Before running `make test` the `fix-whitespace` program should
 # be installed:

src/Algebra/Bundles.agda

@@ -1039,17 +1039,3 @@ record Loop  c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Quasigroup quasigroup public
     using (_≉_; ∙-rawMagma; \\-rawMagma; //-rawMagma)
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 1.0
-
-RawSemigroup = RawMagma
-{-# WARNING_ON_USAGE RawSemigroup
-"Warning: RawSemigroup was deprecated in v1.0.
-Please use RawMagma instead."
-#-}

src/Algebra/FunctionProperties.agda

@@ -6,9 +6,6 @@
 
 {-# OPTIONS --without-K --safe #-}
 
--- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
-
 open import Algebra.Lattice.Bundles
 
 module Algebra.Lattice.Properties.BooleanAlgebra
@@ -17,7 +14,7 @@ module Algebra.Lattice.Properties.BooleanAlgebra
 
 open BooleanAlgebra B
 
-import Algebra.Properties.DistributiveLattice as DistribLatticeProperties
+import Algebra.Lattice.Properties.DistributiveLattice as DistribLatticeProperties
 open import Algebra.Core
 open import Algebra.Structures _≈_
 open import Algebra.Definitions _≈_
@@ -35,7 +32,6 @@ open import Data.Product using (_,_)
 -- Export properties from distributive lattices
 
 open DistribLatticeProperties distributiveLattice public
-  hiding (replace-equality)
 
 ------------------------------------------------------------------------
 -- The dual construction is also a boolean algebra
@@ -139,7 +135,7 @@ open DistribLatticeProperties distributiveLattice public
     ; *-cong = ∧-cong
     ; *-assoc = ∧-assoc
     ; *-identity = ∧-identity
-    ; distrib = ∧-∨-distrib
+    ; distrib = ∧-distrib-∨
     }
   ; zero = ∧-zero
   }
@@ -151,7 +147,7 @@ open DistribLatticeProperties distributiveLattice public
     ; *-cong = ∨-cong
     ; *-assoc = ∨-assoc
     ; *-identity = ∨-identity
-    ; distrib = ∨-∧-distrib
+    ; distrib = ∨-distrib-∧
     }
   ; zero = ∨-zero
   }
@@ -190,10 +186,10 @@ private
   lemma x y x∧y=⊥ x∨y=⊤ = begin
     ¬ x                ≈˘⟨ ∧-identityʳ _ ⟩
     ¬ x ∧ ⊤            ≈˘⟨ ∧-congˡ x∨y=⊤ ⟩
-    ¬ x ∧ (x ∨ y)      ≈⟨  ∧-∨-distribˡ _ _ _ ⟩
+    ¬ x ∧ (x ∨ y)      ≈⟨  ∧-distribˡ-∨ _ _ _ ⟩
     ¬ x ∧ x ∨ ¬ x ∧ y  ≈⟨  ∨-congʳ $ ∧-complementˡ _ ⟩
     ⊥ ∨ ¬ x ∧ y        ≈˘⟨ ∨-congʳ x∧y=⊥ ⟩
-    x ∧ y ∨ ¬ x ∧ y    ≈˘⟨ ∧-∨-distribʳ _ _ _ ⟩
+    x ∧ y ∨ ¬ x ∧ y    ≈˘⟨ ∧-distribʳ-∨ _ _ _ ⟩
     (x ∨ ¬ x) ∧ y      ≈⟨  ∧-congʳ $ ∨-complementʳ _ ⟩
     ⊤ ∧ y              ≈⟨  ∧-identityˡ _ ⟩
     y                  ∎
@@ -211,7 +207,7 @@ deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y
 deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
   where
   lem₁ = begin
-    (x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
+    (x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
     (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∨-congʳ $ ∧-congʳ $ ∧-comm _ _ ⟩
     (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩
     y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y)  ≈⟨ (∧-congˡ $ ∧-complementʳ _) ⟨ ∨-cong ⟩
@@ -279,7 +275,7 @@ module XorRing
   ¬-distribˡ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y
   ¬-distribˡ-⊕ x y = begin
     ¬ (x ⊕ y)                              ≈⟨ ¬-cong $ ⊕-def _ _ ⟩
-    ¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-cong (∧-∨-distribʳ _ _ _) ⟩
+    ¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-cong (∧-distribʳ-∨ _ _ _) ⟩
     ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y)))  ≈⟨ ¬-cong $ ∨-congˡ $ ∧-congˡ $ ¬-cong (∧-comm _ _) ⟩
     ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x)))  ≈⟨ ¬-cong $ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩
     ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x))              ≈⟨ deMorgan₂ _ _ ⟩
@@ -291,7 +287,7 @@ module XorRing
     lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
     lem x y = begin
       x ∧ ¬ (x ∧ y)          ≈⟨ ∧-congˡ $ deMorgan₁ _ _ ⟩
-      x ∧ (¬ x ∨ ¬ y)        ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
+      x ∧ (¬ x ∨ ¬ y)        ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
       (x ∧ ¬ x) ∨ (x ∧ ¬ y)  ≈⟨ ∨-congʳ $ ∧-complementʳ _ ⟩
       ⊥ ∨ (x ∧ ¬ y)          ≈⟨ ∨-identityˡ _ ⟩
       x ∧ ¬ y                ∎
@@ -349,15 +345,15 @@ module XorRing
     (¬ y ∨ ¬ z))               ≈⟨ ∨-congʳ lem₃ ⟩
     ((x ∧ (y ∨ z)) ∧ ¬ x) ∨
     ((x ∧ (y ∨ z)) ∧
-    (¬ y ∨ ¬ z))               ≈˘⟨ ∧-∨-distribˡ _ _ _ ⟩
+    (¬ y ∨ ¬ z))               ≈˘⟨ ∧-distribˡ-∨ _ _ _ ⟩
     (x ∧ (y ∨ z)) ∧
     (¬ x ∨ (¬ y ∨ ¬ z))        ≈˘⟨ ∧-congˡ $ ∨-congˡ (deMorgan₁ _ _) ⟩
     (x ∧ (y ∨ z)) ∧
     (¬ x ∨ ¬ (y ∧ z))          ≈˘⟨ ∧-congˡ (deMorgan₁ _ _) ⟩
     (x ∧ (y ∨ z)) ∧
     ¬ (x ∧ (y ∧ z))            ≈⟨ helper refl lem₁ ⟩
     (x ∧ (y ∨ z)) ∧
-    ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ ∧-congʳ $ ∧-∨-distribˡ _ _ _ ⟩
+    ¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ ∧-congʳ $ ∧-distribˡ-∨ _ _ _ ⟩
     ((x ∧ y) ∨ (x ∧ z)) ∧
     ¬ ((x ∧ y) ∧ (x ∧ z))      ≈˘⟨ ⊕-def _ _ ⟩
     (x ∧ y) ⊕ (x ∧ z)          ∎
@@ -447,7 +443,7 @@ module XorRing
 
     lem₃ = begin
       x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))          ≈⟨ ∨-congˡ $ ∧-congˡ $ deMorgan₁ _ _ ⟩
-      x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
+      x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩
       (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
       ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎
 
@@ -466,7 +462,7 @@ module XorRing
     lem₄ = begin
       ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
       ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ ∨-congˡ lem₄′ ⟩
-      ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
+      ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩
       (¬ x ∨ (y     ∨ ¬ z)) ∧
       (¬ x ∨ (¬ y ∨ z))              ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
       ((¬ x ∨ y)     ∨ ¬ z) ∧
@@ -536,27 +532,6 @@ module XorRing
     { isCommutativeRing = ⊕-∧-isCommutativeRing
     }
 
-  ⊕-¬-distribˡ = ¬-distribˡ-⊕
-  {-# WARNING_ON_USAGE ⊕-¬-distribˡ
-  "Warning: ⊕-¬-distribˡ was deprecated in v1.1.
-  Please use ¬-distribˡ-⊕ instead."
-  #-}
-  ⊕-¬-distribʳ = ¬-distribʳ-⊕
-  {-# WARNING_ON_USAGE ⊕-¬-distribʳ
-  "Warning: ⊕-¬-distribʳ was deprecated in v1.1.
-  Please use ¬-distribʳ-⊕ instead."
-  #-}
-  isCommutativeRing = ⊕-∧-isCommutativeRing
-  {-# WARNING_ON_USAGE isCommutativeRing
-  "Warning: isCommutativeRing was deprecated in v1.1.
-  Please use ⊕-∧-isCommutativeRing instead."
-  #-}
-  commutativeRing = ⊕-∧-commutativeRing
-  {-# WARNING_ON_USAGE commutativeRing
-  "Warning: commutativeRing was deprecated in v1.1.
-  Please use ⊕-∧-commutativeRing instead."
-  #-}
-
 
 infixl 6 _⊕_
 

src/Algebra/FunctionProperties/Core.agda

@@ -467,6 +467,7 @@ module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where
 ------------------------------------------------------------------------
 -- Morphisms over quasigroup-like structures
 ------------------------------------------------------------------------
+
 module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup b ℓ₂) where
 
   open RawQuasigroup Q₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;

src/Algebra/Lattice/Properties/BooleanAlgebra.agda

@@ -6,13 +6,9 @@
 
 {-# OPTIONS --without-K --safe #-}
 
--- Disabled to prevent warnings from deprecated Table
-{-# OPTIONS --warn=noUserWarning #-}
-
 open import Algebra
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.Fin.Base using (Fin; zero)
-open import Data.Table.Base as Table using (Table)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
@@ -40,23 +36,6 @@ open CommutativeMonoid CM
 
 open import Relation.Binary.Reasoning.Setoid setoid
 
--- Summation over lists/tables
-
-sumₗ : List Carrier → Carrier
-sumₗ = List.foldr _+_ 0#
-
-sumₜ : ∀ {n} → Table Carrier n → Carrier
-sumₜ = Table.foldr _+_ 0#
-
--- An alternative mathematical-style syntax for sumₜ
-
-infixl 10 sumₜ-syntax
-
-sumₜ-syntax : ∀ n → (Fin n → Carrier) → Carrier
-sumₜ-syntax _ = sumₜ ∘ Table.tabulate
-
-syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x
-
 ------------------------------------------------------------------------
 -- Multiplication
 

src/Algebra/Morphism/Structures.agda

@@ -38,19 +38,6 @@ open import Data.Product using (_,_)
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
 
--- Version 1.1
-
-¬⊥=⊤ = ⊥≉⊤
-{-# WARNING_ON_USAGE ¬⊥=⊤
-"Warning: ¬⊥=⊤ was deprecated in v1.1.
-Please use ⊥≉⊤ instead."
-#-}
-¬⊤=⊥ = ⊤≉⊥
-{-# WARNING_ON_USAGE ¬⊤=⊥
-"Warning: ¬⊤=⊥ was deprecated in v1.1.
-Please use ⊤≉⊥ instead."
-#-}
-
 -- Version 1.4
 
 replace-equality : {_≈′_ : Rel Carrier b₂} →