From 3bdbdd9421ab57835c9a23bb68a778c63ab302df Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 07:42:49 +0000 Subject: [PATCH 01/20] =?UTF-8?q?[=20breaking=20]=20change=20fieldname=20`?= =?UTF-8?q?=5F=E2=89=9F=5F`=20to=20`=5F=E2=89=88=3F=5F`=20in=20`IsDecEquiv?= =?UTF-8?q?alence`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Relation/Binary/Bundles.agda | 12 ++-- .../Binary/Construct/Flip/EqAndOrd.agda | 4 +- src/Relation/Binary/Properties/DecSetoid.agda | 6 +- src/Relation/Binary/Properties/Setoid.agda | 1 - .../PropositionalEquality/Properties.agda | 4 +- src/Relation/Binary/Structures.agda | 59 ++++++++++++------- 6 files changed, 50 insertions(+), 36 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index cd66369dec..22be21b028 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -64,7 +64,7 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where isDecEquivalence : IsDecEquivalence _≈_ open IsDecEquivalence isDecEquivalence public - using (_≟_; isEquivalence) + using (_≈?_; _≟_; isEquivalence) setoid : Setoid c ℓ setoid = record @@ -140,7 +140,7 @@ record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where private module DPO = IsDecPreorder isDecPreorder open DPO public - using (_≟_; _≲?_; isPreorder) + using (_≈?_; _≲?_; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record @@ -203,7 +203,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where private module DPO = IsDecPartialOrder isDecPartialOrder open DPO public - using (_≟_; _≤?_; isPartialOrder; isDecPreorder) + using (_≈?_; _≤?_; isPartialOrder; isDecPreorder) poset : Poset c ℓ₁ ℓ₂ poset = record @@ -258,7 +258,7 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder open DSPO public - using (_ Date: Wed, 25 Feb 2026 08:11:07 +0000 Subject: [PATCH 02/20] refactor: knock-ons, plus deprecations --- src/Data/Bool/Properties.agda | 25 +++++++--- src/Data/Nat/Properties.agda | 49 +++++++++++++------ .../Binary/Construct/NaturalOrder/Left.agda | 14 +++--- .../Binary/Construct/NonStrictToStrict.agda | 16 +++--- src/Relation/Binary/Construct/On.agda | 6 +-- src/Relation/Binary/Properties/Poset.agda | 2 +- .../Binary/Properties/TotalOrder.agda | 6 +-- .../Binary/PropositionalEquality.agda | 23 +++++++-- 8 files changed, 92 insertions(+), 49 deletions(-) diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda index 53b4a1f4a7..e874cfe85e 100644 --- a/src/Data/Bool/Properties.agda +++ b/src/Data/Bool/Properties.agda @@ -59,19 +59,19 @@ private ------------------------------------------------------------------------ -- Properties of _≡_ -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality Bool -true ≟ true = yes refl -false ≟ false = yes refl -true ≟ false = no λ() -false ≟ true = no λ() +_≡?_ : DecidableEquality Bool +true ≡? true = yes refl +false ≡? false = yes refl +true ≡? false = no λ() +false ≡? true = no λ() ≡-setoid : Setoid 0ℓ 0ℓ ≡-setoid = setoid Bool ≡-decSetoid : DecSetoid 0ℓ 0ℓ -≡-decSetoid = decSetoid _≟_ +≡-decSetoid = decSetoid _≡?_ ------------------------------------------------------------------------ -- Properties of _≤_ @@ -139,7 +139,7 @@ true ≤? true = yes b≤b ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_ ≤-isDecTotalOrder = record { isTotalOrder = ≤-isTotalOrder - ; _≟_ = _≟_ + ; _≈?_ = _≡?_ ; _≤?_ = _≤?_ } @@ -884,3 +884,12 @@ push-function-into-if = if-float "Warning: push-function-into-if was deprecated in v2.0. Please use if-float instead." #-} + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 5976ba29de..1ddc89e2d6 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -104,23 +104,23 @@ suc-injective = cong pred -- We expect the main benefit to be visible in compiled code as the -- backend erases proofs. -infix 4 _≟_ -_≟_ : DecidableEquality ℕ -m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) +infix 4 _≡?_ +_≡?_ : DecidableEquality ℕ +m ≡? n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≡-irrelevant : Irrelevant {A = ℕ} _≡_ -≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_ +≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≡?_ -≟-diag : (eq : m ≡ n) → (m ≟ n) ≡ yes eq -≟-diag = ≡-≟-identity _≟_ +≡?-diag : (eq : m ≡ n) → (m ≡? n) ≡ yes eq +≡?-diag = ≡-≡?-identity _≡?_ -≟-≡ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n -≟-≡ = ≢-≟-identity _≟_ +≡?-≡ : (m≢n : m ≢ n) → (m ≡? n) ≡ no m≢n +≡?-≡ = ≢-≡?-identity _≡?_ ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) ≡-isDecEquivalence = record { isEquivalence = isEquivalence - ; _≟_ = _≟_ + ; _≈?_ = _≡?_ } ≡-decSetoid : DecSetoid 0ℓ 0ℓ @@ -250,7 +250,7 @@ _≥?_ = flip _≤?_ ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_ ≤-isDecTotalOrder = record { isTotalOrder = ≤-isTotalOrder - ; _≟_ = _≟_ + ; _≈?_ = _≡?_ ; _≤?_ = _≤?_ } @@ -400,7 +400,7 @@ n≤1⇒n≡0∨n≡1 (s≤s z≤n) = inj₂ refl -- backend erases proofs. <-cmp : Trichotomous _≡_ _<_ -<-cmp m n with m ≟ n | T? (m <ᵇ n) +<-cmp m n with m ≡? n | T? (m <ᵇ n) ... | yes m≡n | _ = tri≈ (<-irrefl m≡n) m≡n (<-irrefl (sym m≡n)) ... | no m≢n | yes m (m≮n ∘ <⇒<ᵇ) m≢n (≤∧≢⇒< (≮⇒≥ (m≮n ∘ <⇒<ᵇ)) (m≢n ∘ sym)) @@ -2284,7 +2284,7 @@ _>‴?_ = flip _<‴?_ -- decidable equality. eq? : ∀ {a} {A : Set a} → A ↣ ℕ → DecidableEquality A -eq? inj = via-injection inj _≟_ +eq? inj = via-injection inj _≡?_ -- It's possible to decide existential and universal predicates up to -- a limit. @@ -2299,7 +2299,7 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where ... | no ¬Pv | no ¬Pn (x≉y ∘ flip antisym y≤x ∘ proj₁) x≉y (y≤x , x≉y ∘ ≈-sym) <-decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_ -<-decidable _≟_ _≤?_ x y = x ≤? y ×? ¬? (x ≟ y) +<-decidable _≈?_ _≤?_ x y = x ≤? y ×? ¬? (x ≈? y) ------------------------------------------------------------------------ -- Structures @@ -135,18 +135,18 @@ x < y = x ≤ y × x ≉ y IsDecStrictPartialOrder _≈_ _<_ <-isDecStrictPartialOrder dpo = record { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder - ; _≟_ = _≟_ - ; _ Date: Wed, 25 Feb 2026 09:37:49 +0000 Subject: [PATCH 03/20] refactor: MANY MORE knock-ons, plus deprecations --- doc/README/Data/Trie/NonDependent.agda | 4 +- src/Data/Char/Properties.agda | 31 +++++--- src/Data/Fin/Permutation.agda | 28 ++++---- src/Data/Fin/Permutation/Components.agda | 24 +++---- src/Data/Fin/Properties.agda | 70 +++++++++++++------ src/Data/Integer.agda | 2 +- src/Data/Integer/Properties.agda | 26 ++++--- src/Data/List/Relation/Binary/Lex/Strict.agda | 4 +- src/Data/List/Relation/Binary/Pointwise.agda | 2 +- .../List/Relation/Unary/Any/Properties.agda | 4 +- src/Data/Nat/DivMod/Core.agda | 2 +- src/Data/Nat/Divisibility.agda | 2 +- .../Binary/Pointwise/NonDependent.agda | 2 +- src/Data/String.agda | 6 +- src/Data/String/Properties.agda | 33 ++++++--- src/Data/Sum/Relation/Binary/Pointwise.agda | 2 +- src/Data/Unit.agda | 2 +- src/Data/Unit/Polymorphic/Properties.agda | 28 ++++++-- src/Data/Unit/Properties.agda | 28 ++++++-- .../Construct/Add/Infimum/NonStrict.agda | 8 +-- .../Binary/Construct/Add/Infimum/Strict.agda | 4 +- .../Binary/Construct/Add/Point/Equality.agda | 2 +- .../Construct/Add/Supremum/NonStrict.agda | 8 +-- .../Binary/Construct/Add/Supremum/Strict.agda | 4 +- .../Closure/Reflexive/Properties.agda | 4 +- .../Binary/Construct/Intersection.agda | 2 +- .../Binary/Properties/DecTotalOrder.agda | 2 +- 27 files changed, 214 insertions(+), 120 deletions(-) diff --git a/doc/README/Data/Trie/NonDependent.agda b/doc/README/Data/Trie/NonDependent.agda index 385e981880..f367b78587 100644 --- a/doc/README/Data/Trie/NonDependent.agda +++ b/doc/README/Data/Trie/NonDependent.agda @@ -83,7 +83,7 @@ record Lexer t : Set (suc t) where -- Two keywords are considered distinct if the strings are not equal Distinct : Rel Keyword 0ℓ - Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋ + Distinct a b = ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋ field @@ -175,7 +175,7 @@ module LetIn where LPAR RPAR : TOK ID : String → TOK - keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋) + keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋) keywords = ("let" , LET) ∷# ("=" , EQ) ∷# ("in" , IN) diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda index 9e515f7e3a..5d158e6ae7 100644 --- a/src/Data/Char/Properties.agda +++ b/src/Data/Char/Properties.agda @@ -14,7 +14,7 @@ import Data.Nat.Base as ℕ using (ℕ; _<_; _≤_) import Data.Nat.Properties as ℕ using (_0 mod≢0) mod≤1+j , j≤k)) divₕ-offsetEq d (suc n) (suc j) (suc k) j≤d k≤d (inj₃ (eq , k Date: Wed, 25 Feb 2026 12:16:17 +0000 Subject: [PATCH 04/20] refactor: last round of knock-ons --- doc/README/Data/List/Membership.agda | 4 +- .../Data/List/Relation/Binary/Subset.agda | 4 +- doc/README/Data/Record.agda | 2 +- doc/README/Foreign/Haskell.agda | 4 +- doc/README/Function/Reasoning.agda | 2 +- doc/README/Nary.agda | 4 +- .../Solver/CommutativeMonoid/Normal.agda | 15 +- .../IdempotentCommutativeMonoid/Normal.agda | 15 +- src/Algebra/Solver/Monoid/Normal.agda | 25 +- .../Ring/NaturalCoefficients/Default.agda | 4 +- src/Data/Bool.agda | 2 +- src/Data/Bool/Instances.agda | 4 +- src/Data/Bool/Solver.agda | 6 +- src/Data/Char.agda | 2 +- src/Data/Digit/Properties.agda | 2 +- src/Data/Fin.agda | 2 +- src/Data/Fin/Subset.agda | 4 +- src/Data/Fin/Subset/Properties.agda | 4 +- src/Data/Float.agda | 2 +- src/Data/Float/Instances.agda | 4 +- src/Data/Float/Properties.agda | 30 +- src/Data/Graph/Acyclic.agda | 4 +- src/Data/Integer/Divisibility/Signed.agda | 2 +- src/Data/Integer/Instances.agda | 4 +- src/Data/Integer/Solver.agda | 4 +- src/Data/List/Instances.agda | 4 +- .../Binary/Infix/Homogeneous/Properties.agda | 2 +- .../List/Relation/Binary/Lex/NonStrict.agda | 6 +- .../Binary/Prefix/Homogeneous/Properties.agda | 2 +- .../Binary/Sublist/DecPropositional.agda | 8 +- .../Relation/Binary/Sublist/DecSetoid.agda | 4 +- .../Sublist/Heterogeneous/Properties.agda | 2 +- .../Binary/Sublist/Heterogeneous/Solver.agda | 2 +- .../Binary/Suffix/Homogeneous/Properties.agda | 2 +- src/Data/Maybe/Relation/Binary/Pointwise.agda | 2 +- src/Data/Nat.agda | 2 +- src/Data/Nat/Binary/Instances.agda | 4 +- src/Data/Nat/Binary/Properties.agda | 39 +- src/Data/Nat/Combinatorics/Specification.agda | 2 +- src/Data/Nat/Coprimality.agda | 2 +- src/Data/Nat/GCD.agda | 2 +- src/Data/Nat/Instances.agda | 4 +- src/Data/Nat/Primality.agda | 4 +- src/Data/Nat/Solver.agda | 2 +- src/Data/Product/Instances.agda | 2 +- .../Relation/Binary/Lex/NonStrict.agda | 6 +- src/Data/Rational/Instances.agda | 4 +- src/Data/Rational/Properties.agda | 23 +- src/Data/Rational/Solver.agda | 4 +- .../Rational/Unnormalised/Properties.agda | 6 +- src/Data/String/Instances.agda | 4 +- src/Data/Sum/Instances.agda | 4 +- src/Data/Sum/Relation/Binary/LeftOrder.agda | 2 +- src/Data/These/Instances.agda | 4 +- .../Membership/Propositional/Properties.agda | 2 +- .../Tree/AVL/Sets/Membership/Properties.agda | 2 +- src/Data/Unit/Instances.agda | 4 +- src/Data/Unit/Polymorphic/Instances.agda | 4 +- .../Relation/Binary/Pointwise/Properties.agda | 2 +- src/Data/Vec/Instances.agda | 4 +- src/Data/Vec/Relation/Binary/Lex/Core.agda | 4 +- src/Data/Vec/Relation/Binary/Lex/Strict.agda | 12 +- .../Binary/Pointwise/Extensional.agda | 2 +- .../Relation/Binary/Pointwise/Inductive.agda | 2 +- src/Data/Word64/Instances.agda | 4 +- src/Data/Word64/Properties.agda | 29 +- src/Reflection.agda | 64 +- src/Reflection/AST/Abstraction.agda | 8 +- src/Reflection/AST/AlphaEquality.agda | 12 +- src/Reflection/AST/Argument.agda | 4 +- src/Reflection/AST/Argument/Information.agda | 24 +- src/Reflection/AST/Argument/Modality.agda | 25 +- src/Reflection/AST/Argument/Quantity.agda | 27 +- src/Reflection/AST/Argument/Relevance.agda | 27 +- src/Reflection/AST/Argument/Visibility.agda | 38 +- src/Reflection/AST/Definition.agda | 92 +-- src/Reflection/AST/Instances.agda | 26 +- src/Reflection/AST/Literal.agda | 119 ++-- src/Reflection/AST/Meta.agda | 26 +- src/Reflection/AST/Name.agda | 26 +- src/Reflection/AST/Pattern.agda | 4 +- src/Reflection/AST/Term.agda | 548 ++++++++++-------- src/Relation/Binary/Construct/Flip/Ord.agda | 4 +- .../Binary/Construct/Interior/Symmetric.agda | 2 +- .../Binary/Construct/NaturalOrder/Right.agda | 12 +- .../Binary/Construct/StrictToNonStrict.agda | 2 +- .../Binary/HeterogeneousEquality.agda | 2 +- .../Indexed/Homogeneous/Construct/At.agda | 2 +- .../Indexed/Homogeneous/Structures.agda | 10 +- .../Lattice/Properties/JoinSemilattice.agda | 6 +- .../Lattice/Properties/MeetSemilattice.agda | 8 +- .../Binary/Morphism/OrderMonomorphism.agda | 2 +- .../Binary/Morphism/RelMonomorphism.agda | 2 +- src/Relation/Binary/TypeClasses.agda | 2 +- src/Tactic/Cong.agda | 2 +- src/Test/Golden.agda | 8 +- src/Text/Regex/Properties.agda | 2 +- 97 files changed, 903 insertions(+), 613 deletions(-) diff --git a/doc/README/Data/List/Membership.agda b/doc/README/Data/List/Membership.agda index 38732fe631..d29a2cf9d8 100644 --- a/doc/README/Data/List/Membership.agda +++ b/doc/README/Data/List/Membership.agda @@ -34,7 +34,7 @@ import Data.List.Membership.DecPropositional as DecPropMembership -- propositional equality over `ℕ` and it is also decidable. Therefore -- the module `DecPropMembership` should be opened as follows: -open DecPropMembership ℕ._≟_ +open DecPropMembership ℕ._≡?_ -- As membership is just an instance of `Any` we also need to import -- the constructors `here` and `there`. (See issue #553 on Github for @@ -66,7 +66,7 @@ import Data.List.Membership.Propositional.Properties as PropProperties -- following the first `∈` refers to lists of type `List ℕ` whereas -- the second `∈` refers to lists of type `List Char`. -open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_) +open DecPropMembership Char._≡?_ renaming (_∈_ to _∈ᶜ_) open SetoidProperties using (∈-map⁺) lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs diff --git a/doc/README/Data/List/Relation/Binary/Subset.agda b/doc/README/Data/List/Relation/Binary/Subset.agda index ccef725cca..646c4c6e54 100644 --- a/doc/README/Data/List/Relation/Binary/Subset.agda +++ b/doc/README/Data/List/Relation/Binary/Subset.agda @@ -22,10 +22,10 @@ module README.Data.List.Relation.Binary.Subset where -- Decidable equality over Strings open import Data.String.Base using (String) -open import Data.String.Properties using (_≟_) +open import Data.String.Properties using (_≡?_) -- Open the decidable membership module using Decidable ≡ over Strings -open import Data.List.Membership.DecPropositional _≟_ +open import Data.List.Membership.DecPropositional _≡?_ -- Simple cases are inductive proofs diff --git a/doc/README/Data/Record.agda b/doc/README/Data/Record.agda index 63fea328ae..53b3d50fb2 100644 --- a/doc/README/Data/Record.agda +++ b/doc/README/Data/Record.agda @@ -21,7 +21,7 @@ import Data.Record as Record -- Let us use strings as labels. -open Record String _≟_ +open Record String _≡?_ -- Partial equivalence relations. diff --git a/doc/README/Foreign/Haskell.agda b/doc/README/Foreign/Haskell.agda index 38c6c78c4e..e608334197 100644 --- a/doc/README/Foreign/Haskell.agda +++ b/doc/README/Foreign/Haskell.agda @@ -92,12 +92,12 @@ main = run $ do content ← readFiniteFile "README/Foreign/Haskell.agda" let chars = toList content let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing) - let cleaned = dropWhile ('\n' ≟_) $ cleanup chars + let cleaned = dropWhile ('\n' ≡?_) $ cleanup chars case uncons cleaned of λ where nothing → putStrLn "I cannot believe this file is filed with dashes only!" (just (c , cs)) → putStrLn $ unlines $ ("First (non dash) character: " ++ Char.show c) - ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≟_)) cs)) + ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≡?_)) cs)) ∷ [] -- You can compile and run this test by writing: diff --git a/doc/README/Function/Reasoning.agda b/doc/README/Function/Reasoning.agda index 810f048aa3..7c2d3ed7d0 100644 --- a/doc/README/Function/Reasoning.agda +++ b/doc/README/Function/Reasoning.agda @@ -57,7 +57,7 @@ subpalindromes str = let Chars = List Char in |> filter (λ cs → 2 ≤? length cs) ∶ List Chars -- only keep the ones that are palindromes |> map < fromList , fromList ∘ reverse > ∶ List (String × String) - |> filter (uncurry String._≟_) ∶ List (String × String) + |> filter (uncurry String._≡?_) ∶ List (String × String) |> map proj₁ ∶ List String -- Test cases diff --git a/doc/README/Nary.agda b/doc/README/Nary.agda index b8b337832a..e06c3a8455 100644 --- a/doc/README/Nary.agda +++ b/doc/README/Nary.agda @@ -338,14 +338,14 @@ exist₁ = 19 , 793 , 3059 , 10 , refl -- ∀[_] P = ∀ {a₁} → ⋯ → ∀ {aₙ} → P a₁ ⋯ aₙ all₁ : ∀[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ] -all₁ {a₁} {a₂} = a₁ ≟ a₂ +all₁ {a₁} {a₂} = a₁ ≡? a₂ ------------------------------------------------------------------------ -- Π : (A₁ → ⋯ → Aₙ → Set r) → Set _ -- Π P = ∀ a₁ → ⋯ → ∀ aₙ → P a₁ ⋯ aₙ all₂ : Π[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ] -all₂ = _≟_ +all₂ = _≡?_ ------------------------------------------------------------------------ -- _⇒_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _) diff --git a/src/Algebra/Solver/CommutativeMonoid/Normal.agda b/src/Algebra/Solver/CommutativeMonoid/Normal.agda index 7713e497e1..ae564c1f0a 100644 --- a/src/Algebra/Solver/CommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/CommutativeMonoid/Normal.agda @@ -57,10 +57,10 @@ Normal n = Vec ℕ n -- We can decide if two normal forms are /syntactically/ equal. -infix 5 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≟_ nf₁ nf₂) +_≡?_ : DecidableEquality (Normal n) +nf₁ ≡? nf₂ = Dec.map Pointwise-≡↔≡ (decidable ℕ._≡?_ nf₁ nf₂) where open Pointwise using (Pointwise-≡↔≡; decidable) ------------------------------------------------------------------------ @@ -162,3 +162,12 @@ sg-correct = singleton-correct "Warning: sg-correct was deprecated in v2.2. Please use singleton-correct instead." #-} + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda index 0ebdf4351d..4c67728c65 100644 --- a/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda +++ b/src/Algebra/Solver/IdempotentCommutativeMonoid/Normal.agda @@ -56,10 +56,10 @@ Normal n = Vec Bool n -- We can decide if two normal forms are /syntactically/ equal. -infix 5 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≟_ nf₁ nf₂) +_≡?_ : DecidableEquality (Normal n) +nf₁ ≡? nf₂ = Dec.map Pointwise-≡↔≡ (decidable Bool._≡?_ nf₁ nf₂) where open Pointwise using (Pointwise-≡↔≡; decidable) ------------------------------------------------------------------------ @@ -167,3 +167,12 @@ sg-correct = singleton-correct "Warning: sg-correct was deprecated in v2.2. Please use singleton-correct instead." #-} + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 62a02bfca5..2195eeafac 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -50,11 +50,11 @@ Normal n = List (Fin n) -- We can decide if two normal forms are /syntactically/ equal. -infix 5 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality (Normal n) -nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) - where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋) +_≡?_ : DecidableEquality (Normal n) +nf₁ ≡? nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂) + where open ≋ Fin._≡?_ using (_≋?_; ≋⇒≡; ≡⇒≋) -- A normaliser. @@ -87,3 +87,20 @@ correct (e₁ ⊕ e₂) ρ = begin ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩ ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩ ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ ∎ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ + +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda index 324f05eb04..89d4ab537b 100644 --- a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda +++ b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda @@ -18,7 +18,7 @@ module Algebra.Solver.Ring.NaturalCoefficients.Default import Algebra.Properties.Semiring.Mult as SemiringMultiplication using (_×_) open import Data.Maybe.Base using (Maybe; map) -open import Data.Nat using (_≟_) +open import Data.Nat using (_≡?_) open import Relation.Binary.Consequences using (dec⇒weaklyDec) import Relation.Binary.PropositionalEquality.Core as ≡ using (refl; cong) @@ -27,6 +27,6 @@ open SemiringMultiplication semiring private dec : ∀ m n → Maybe (m × 1# ≈ n × 1#) - dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≟_ m n) + dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≡?_ m n) open import Algebra.Solver.Ring.NaturalCoefficients R dec public diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda index 55ed146e2c..0ead2d50b2 100644 --- a/src/Data/Bool.agda +++ b/src/Data/Bool.agda @@ -17,4 +17,4 @@ open import Data.Bool.Base public -- Publicly re-export queries open import Data.Bool.Properties public - using (T?; _≟_; _≤?_; _?_ ; ≤-<-connex ; ≥->-connex ; <-≤-connex ; >-≥-connex diff --git a/src/Data/Nat/Binary/Instances.agda b/src/Data/Nat/Binary/Instances.agda index 9ef0ef6373..f8c56ebc38 100644 --- a/src/Data/Nat/Binary/Instances.agda +++ b/src/Data/Nat/Binary/Instances.agda @@ -8,9 +8,9 @@ module Data.Nat.Binary.Instances where -open import Data.Nat.Binary.Properties +open import Data.Nat.Binary.Properties using (_≡?_) open import Relation.Binary.PropositionalEquality.Properties using (isDecEquivalence) instance - ℕᵇ-≡-isDecEquivalence = isDecEquivalence _≟_ + ℕᵇ-≡-isDecEquivalence = isDecEquivalence _≡?_ diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index 6c2298d88a..79ca4687d2 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -61,7 +61,7 @@ private variable x : ℕᵇ -infix 4 _; uncurry) open import Level using (Level) open import Relation.Nullary.Decidable.Core using (Dec; map′; _×?_) @@ -58,8 +58,8 @@ unAbs : Abs A → A unAbs (abs s a) = a unAbs-dec : {abs1 abs2 : Abs A} → Dec (unAbs abs1 ≡ unAbs abs2) → Dec (abs1 ≡ abs2) -unAbs-dec {abs1 = abs s a} {abs t a′} a≟a′ = - map′ (uncurry (cong₂ abs)) abs-injective (s String.≟ t ×? a≟a′) +unAbs-dec {abs1 = abs s a} {abs t a′} a≡?a′ = + map′ (uncurry (cong₂ abs)) abs-injective (s String.≡? t ×? a≡?a′) ≡-dec : DecidableEquality A → DecidableEquality (Abs A) -≡-dec _≟_ x y = unAbs-dec (unAbs x ≟ unAbs y) +≡-dec _≡?_ x y = unAbs-dec (unAbs x ≡? unAbs y) diff --git a/src/Reflection/AST/AlphaEquality.agda b/src/Reflection/AST/AlphaEquality.agda index fc2e3bfcd5..f6d1a7b1b5 100644 --- a/src/Reflection/AST/AlphaEquality.agda +++ b/src/Reflection/AST/AlphaEquality.agda @@ -55,22 +55,22 @@ open AlphaEquality {{...}} public instance α-Visibility : AlphaEquality Visibility - α-Visibility = ≟⇒α Visibility._≟_ + α-Visibility = ≟⇒α Visibility._≡?_ α-Modality : AlphaEquality Modality - α-Modality = ≟⇒α Modality._≟_ + α-Modality = ≟⇒α Modality._≡?_ α-ArgInfo : AlphaEquality ArgInfo - α-ArgInfo = ≟⇒α ArgInfo._≟_ + α-ArgInfo = ≟⇒α ArgInfo._≡?_ α-Literal : AlphaEquality Literal - α-Literal = ≟⇒α Literal._≟_ + α-Literal = ≟⇒α Literal._≡?_ α-Meta : AlphaEquality Meta - α-Meta = ≟⇒α Meta._≟_ + α-Meta = ≟⇒α Meta._≡?_ α-Name : AlphaEquality Name - α-Name = ≟⇒α Name._≟_ + α-Name = ≟⇒α Name._≡?_ ------------------------------------------------------------------------ -- Interesting cases diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda index 9fd29e7330..5582e5b4a9 100644 --- a/src/Reflection/AST/Argument.agda +++ b/src/Reflection/AST/Argument.agda @@ -86,7 +86,7 @@ unArg (arg i a) = a unArg-dec : {arg1 arg2 : Arg A} → Dec (unArg arg1 ≡ unArg arg2) → Dec (arg1 ≡ arg2) unArg-dec {arg1 = arg i x} {arg j y} arg1≟arg2 = - map′ (uncurry (cong₂ arg)) arg-injective (i Information.≟ j ×? arg1≟arg2) + map′ (uncurry (cong₂ arg)) arg-injective (i Information.≡? j ×? arg1≟arg2) ≡-dec : DecidableEquality A → DecidableEquality (Arg A) -≡-dec _≟_ x y = unArg-dec (unArg x ≟ unArg y) +≡-dec _≡?_ x y = unArg-dec (unArg x ≡? unArg y) diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda index 307a1b1976..6940c3c492 100644 --- a/src/Reflection/AST/Argument/Information.agda +++ b/src/Reflection/AST/Argument/Information.agda @@ -47,11 +47,27 @@ arg-info-injective₂ refl = refl arg-info-injective : arg-info v m ≡ arg-info v′ m′ → v ≡ v′ × m ≡ m′ arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ > -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality ArgInfo -arg-info v m ≟ arg-info v′ m′ = +_≡?_ : DecidableEquality ArgInfo +arg-info v m ≡? arg-info v′ m′ = map′ (uncurry (cong₂ arg-info)) arg-info-injective - (v Visibility.≟ v′ ×? m Modality.≟ m′) + (v Visibility.≡? v′ ×? m Modality.≡? m′) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda index e71b0f2710..61886cad95 100644 --- a/src/Reflection/AST/Argument/Modality.agda +++ b/src/Reflection/AST/Argument/Modality.agda @@ -47,11 +47,28 @@ modality-injective₂ refl = refl modality-injective : modality r q ≡ modality r′ q′ → r ≡ r′ × q ≡ q′ modality-injective = < modality-injective₁ , modality-injective₂ > -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality Modality -modality r q ≟ modality r′ q′ = +_≡?_ : DecidableEquality Modality +modality r q ≡? modality r′ q′ = map′ (uncurry (cong₂ modality)) modality-injective - (r Relevance.≟ r′ ×? q Quantity.≟ q′) + (r Relevance.≡? r′ ×? q Quantity.≡? q′) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ + +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda index a042218660..6d1a0a7fc2 100644 --- a/src/Reflection/AST/Argument/Quantity.agda +++ b/src/Reflection/AST/Argument/Quantity.agda @@ -21,10 +21,27 @@ open Quantity public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≡?_ + +_≡?_ : DecidableEquality Quantity +quantity-ω ≡? quantity-ω = yes refl +quantity-0 ≡? quantity-0 = yes refl +quantity-ω ≡? quantity-0 = no λ() +quantity-0 ≡? quantity-ω = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + infix 4 _≟_ -_≟_ : DecidableEquality Quantity -quantity-ω ≟ quantity-ω = yes refl -quantity-0 ≟ quantity-0 = yes refl -quantity-ω ≟ quantity-0 = no λ() -quantity-0 ≟ quantity-ω = no λ() +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda index a06095dc8b..c4020c350e 100644 --- a/src/Reflection/AST/Argument/Relevance.agda +++ b/src/Reflection/AST/Argument/Relevance.agda @@ -21,10 +21,27 @@ open Relevance public ------------------------------------------------------------------------ -- Decidable equality +infix 4 _≡?_ + +_≡?_ : DecidableEquality Relevance +relevant ≡? relevant = yes refl +irrelevant ≡? irrelevant = yes refl +relevant ≡? irrelevant = no λ() +irrelevant ≡? relevant = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + infix 4 _≟_ -_≟_ : DecidableEquality Relevance -relevant ≟ relevant = yes refl -irrelevant ≟ irrelevant = yes refl -relevant ≟ irrelevant = no λ() -irrelevant ≟ relevant = no λ() +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda index db68cb4b27..35f7133346 100644 --- a/src/Reflection/AST/Argument/Visibility.agda +++ b/src/Reflection/AST/Argument/Visibility.agda @@ -21,15 +21,31 @@ open Visibility public ------------------------------------------------------------------------ -- Decidable equality -infix 4 _≟_ +infix 4 _≡?_ + +_≡?_ : DecidableEquality Visibility +visible ≡? visible = yes refl +hidden ≡? hidden = yes refl +instance′ ≡? instance′ = yes refl +visible ≡? hidden = no λ() +visible ≡? instance′ = no λ() +hidden ≡? visible = no λ() +hidden ≡? instance′ = no λ() +instance′ ≡? visible = no λ() +instance′ ≡? hidden = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. -_≟_ : DecidableEquality Visibility -visible ≟ visible = yes refl -hidden ≟ hidden = yes refl -instance′ ≟ instance′ = yes refl -visible ≟ hidden = no λ() -visible ≟ instance′ = no λ() -hidden ≟ visible = no λ() -hidden ≟ instance′ = no λ() -instance′ ≟ visible = no λ() -instance′ ≟ hidden = no λ() +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda index 400499afd3..75c9447bec 100644 --- a/src/Reflection/AST/Definition.agda +++ b/src/Reflection/AST/Definition.agda @@ -9,15 +9,15 @@ module Reflection.AST.Definition where import Data.List.Properties as List using (≡-dec) -import Data.Nat.Properties as ℕ using (_≟_) +import Data.Nat.Properties as ℕ using (_≡?_) open import Data.Product.Base using (_×_; <_,_>; uncurry) open import Relation.Nullary.Decidable.Core using (map′; _×?_; yes; no) open import Relation.Binary.Definitions using (DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) import Reflection.AST.Argument as Arg using (Arg; ≡-dec) -import Reflection.AST.Argument.Quantity as Quantity using (Quantity; _≟_) -import Reflection.AST.Name as Name using (Name; _≟_) -import Reflection.AST.Term as Term using (Term; _≟-Clauses_) +import Reflection.AST.Argument.Quantity as Quantity using (Quantity; _≡?_) +import Reflection.AST.Name as Name using (Name; _≡?_) +import Reflection.AST.Term as Term using (Term; _≡?-Clauses_) ------------------------------------------------------------------------ -- Re-exporting type publicly @@ -65,51 +65,51 @@ constructor′-injective₂ refl = refl constructor′-injective : ∀ {c c′ q q′} → constructor′ c q ≡ constructor′ c′ q′ → c ≡ c′ × q ≡ q′ constructor′-injective = < constructor′-injective₁ , constructor′-injective₂ > -infix 4 _≟_ +infix 4 _≡?_ -_≟_ : DecidableEquality Definition -function cs ≟ function cs′ = - map′ (cong function) function-injective (cs Term.≟-Clauses cs′) -data-type pars cs ≟ data-type pars′ cs′ = +_≡?_ : DecidableEquality Definition +function cs ≡? function cs′ = + map′ (cong function) function-injective (cs Term.≡?-Clauses cs′) +data-type pars cs ≡? data-type pars′ cs′ = map′ (uncurry (cong₂ data-type)) data-type-injective - (pars ℕ.≟ pars′ ×? List.≡-dec Name._≟_ cs cs′) -record′ c fs ≟ record′ c′ fs′ = + (pars ℕ.≡? pars′ ×? List.≡-dec Name._≡?_ cs cs′) +record′ c fs ≡? record′ c′ fs′ = map′ (uncurry (cong₂ record′)) record′-injective - (c Name.≟ c′ ×? List.≡-dec (Arg.≡-dec Name._≟_) fs fs′) -constructor′ d q ≟ constructor′ d′ q′ = + (c Name.≡? c′ ×? List.≡-dec (Arg.≡-dec Name._≡?_) fs fs′) +constructor′ d q ≡? constructor′ d′ q′ = map′ (uncurry (cong₂ constructor′)) constructor′-injective - (d Name.≟ d′ ×? q Quantity.≟ q′) -axiom ≟ axiom = yes refl -primitive′ ≟ primitive′ = yes refl + (d Name.≡? d′ ×? q Quantity.≡? q′) +axiom ≡? axiom = yes refl +primitive′ ≡? primitive′ = yes refl -- antidiagonal -function cs ≟ data-type pars cs₁ = no (λ ()) -function cs ≟ record′ c fs = no (λ ()) -function cs ≟ constructor′ d q = no (λ ()) -function cs ≟ axiom = no (λ ()) -function cs ≟ primitive′ = no (λ ()) -data-type pars cs ≟ function cs₁ = no (λ ()) -data-type pars cs ≟ record′ c fs = no (λ ()) -data-type pars cs ≟ constructor′ d q = no (λ ()) -data-type pars cs ≟ axiom = no (λ ()) -data-type pars cs ≟ primitive′ = no (λ ()) -record′ c fs ≟ function cs = no (λ ()) -record′ c fs ≟ data-type pars cs = no (λ ()) -record′ c fs ≟ constructor′ d q = no (λ ()) -record′ c fs ≟ axiom = no (λ ()) -record′ c fs ≟ primitive′ = no (λ ()) -constructor′ d q ≟ function cs = no (λ ()) -constructor′ d q ≟ data-type pars cs = no (λ ()) -constructor′ d q ≟ record′ c fs = no (λ ()) -constructor′ d q ≟ axiom = no (λ ()) -constructor′ d q ≟ primitive′ = no (λ ()) -axiom ≟ function cs = no (λ ()) -axiom ≟ data-type pars cs = no (λ ()) -axiom ≟ record′ c fs = no (λ ()) -axiom ≟ constructor′ d q = no (λ ()) -axiom ≟ primitive′ = no (λ ()) -primitive′ ≟ function cs = no (λ ()) -primitive′ ≟ data-type pars cs = no (λ ()) -primitive′ ≟ record′ c fs = no (λ ()) -primitive′ ≟ constructor′ d q = no (λ ()) -primitive′ ≟ axiom = no (λ ()) +function cs ≡? data-type pars cs₁ = no (λ ()) +function cs ≡? record′ c fs = no (λ ()) +function cs ≡? constructor′ d q = no (λ ()) +function cs ≡? axiom = no (λ ()) +function cs ≡? primitive′ = no (λ ()) +data-type pars cs ≡? function cs₁ = no (λ ()) +data-type pars cs ≡? record′ c fs = no (λ ()) +data-type pars cs ≡? constructor′ d q = no (λ ()) +data-type pars cs ≡? axiom = no (λ ()) +data-type pars cs ≡? primitive′ = no (λ ()) +record′ c fs ≡? function cs = no (λ ()) +record′ c fs ≡? data-type pars cs = no (λ ()) +record′ c fs ≡? constructor′ d q = no (λ ()) +record′ c fs ≡? axiom = no (λ ()) +record′ c fs ≡? primitive′ = no (λ ()) +constructor′ d q ≡? function cs = no (λ ()) +constructor′ d q ≡? data-type pars cs = no (λ ()) +constructor′ d q ≡? record′ c fs = no (λ ()) +constructor′ d q ≡? axiom = no (λ ()) +constructor′ d q ≡? primitive′ = no (λ ()) +axiom ≡? function cs = no (λ ()) +axiom ≡? data-type pars cs = no (λ ()) +axiom ≡? record′ c fs = no (λ ()) +axiom ≡? constructor′ d q = no (λ ()) +axiom ≡? primitive′ = no (λ ()) +primitive′ ≡? function cs = no (λ ()) +primitive′ ≡? data-type pars cs = no (λ ()) +primitive′ ≡? record′ c fs = no (λ ()) +primitive′ ≡? constructor′ d q = no (λ ()) +primitive′ ≡? axiom = no (λ ()) diff --git a/src/Reflection/AST/Instances.agda b/src/Reflection/AST/Instances.agda index 27a766076d..8d0971d71d 100644 --- a/src/Reflection/AST/Instances.agda +++ b/src/Reflection/AST/Instances.agda @@ -33,20 +33,20 @@ private A : Set a instance - Lit-≡-isDecEquivalence = isDecEquivalence Literal._≟_ - Name-≡-isDecEquivalence = isDecEquivalence Name._≟_ - Meta-≡-isDecEquivalence = isDecEquivalence Meta._≟_ - Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≟_ - Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≟_ - Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≟_ - ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≟_ - Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≟_ - Clause-≡-isDecEquivalence = isDecEquivalence Term._≟-Clause_ - Term-≡-isDecEquivalence = isDecEquivalence Term._≟_ - Sort-≡-isDecEquivalence = isDecEquivalence Term._≟-Sort_ + Lit-≡-isDecEquivalence = isDecEquivalence Literal._≡?_ + Name-≡-isDecEquivalence = isDecEquivalence Name._≡?_ + Meta-≡-isDecEquivalence = isDecEquivalence Meta._≡?_ + Visibility-≡-isDecEquivalence = isDecEquivalence Visibility._≡?_ + Relevance-≡-isDecEquivalence = isDecEquivalence Relevance._≡?_ + Quantity-≡-isDecEquivalence = isDecEquivalence Quantity._≡?_ + ArgInfo-≡-isDecEquivalence = isDecEquivalence Information._≡?_ + Pattern-≡-isDecEquivalence = isDecEquivalence Pattern._≡?_ + Clause-≡-isDecEquivalence = isDecEquivalence Term._≡?-Clause_ + Term-≡-isDecEquivalence = isDecEquivalence Term._≡?_ + Sort-≡-isDecEquivalence = isDecEquivalence Term._≡?-Sort_ Abs-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = Abstraction.Abs A} _≡_ - Abs-≡-isDecEquivalence = isDecEquivalence (Abstraction.≡-dec _≟_) + Abs-≡-isDecEquivalence = isDecEquivalence (Abstraction.≡-dec _≈?_) Arg-≡-isDecEquivalence : {{IsDecEquivalence {A = A} _≡_}} → IsDecEquivalence {A = Argument.Arg A} _≡_ - Arg-≡-isDecEquivalence = isDecEquivalence (Argument.≡-dec _≟_) + Arg-≡-isDecEquivalence = isDecEquivalence (Argument.≡-dec _≈?_) diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda index 9048e75ede..27e7c87816 100644 --- a/src/Reflection/AST/Literal.agda +++ b/src/Reflection/AST/Literal.agda @@ -51,59 +51,74 @@ string-injective refl = refl name-injective : ∀ {x y} → name x ≡ name y → x ≡ y name-injective refl = refl -infix 4 _≟_ -_≟_ : DecidableEquality Literal -nat x ≟ nat x₁ = map′ (cong nat) nat-injective (x ℕ.≟ x₁) -nat x ≟ word64 x₁ = no (λ ()) -nat x ≟ float x₁ = no (λ ()) -nat x ≟ char x₁ = no (λ ()) -nat x ≟ string x₁ = no (λ ()) -nat x ≟ name x₁ = no (λ ()) -nat x ≟ meta x₁ = no (λ ()) -word64 x ≟ word64 x₁ = map′ (cong word64) word64-injective (x Word64.≟ x₁) -word64 x ≟ nat x₁ = no (λ ()) -word64 x ≟ float x₁ = no (λ ()) -word64 x ≟ char x₁ = no (λ ()) -word64 x ≟ string x₁ = no (λ ()) -word64 x ≟ name x₁ = no (λ ()) -word64 x ≟ meta x₁ = no (λ ()) -float x ≟ nat x₁ = no (λ ()) -float x ≟ word64 x₁ = no (λ ()) -float x ≟ float x₁ = map′ (cong float) float-injective (x Float.≟ x₁) -float x ≟ char x₁ = no (λ ()) -float x ≟ string x₁ = no (λ ()) -float x ≟ name x₁ = no (λ ()) -float x ≟ meta x₁ = no (λ ()) -char x ≟ nat x₁ = no (λ ()) -char x ≟ word64 x₁ = no (λ ()) -char x ≟ float x₁ = no (λ ()) -char x ≟ char x₁ = map′ (cong char) char-injective (x Char.≟ x₁) -char x ≟ string x₁ = no (λ ()) -char x ≟ name x₁ = no (λ ()) -char x ≟ meta x₁ = no (λ ()) -string x ≟ nat x₁ = no (λ ()) -string x ≟ word64 x₁ = no (λ ()) -string x ≟ float x₁ = no (λ ()) -string x ≟ char x₁ = no (λ ()) -string x ≟ string x₁ = map′ (cong string) string-injective (x String.≟ x₁) -string x ≟ name x₁ = no (λ ()) -string x ≟ meta x₁ = no (λ ()) -name x ≟ nat x₁ = no (λ ()) -name x ≟ word64 x₁ = no (λ ()) -name x ≟ float x₁ = no (λ ()) -name x ≟ char x₁ = no (λ ()) -name x ≟ string x₁ = no (λ ()) -name x ≟ name x₁ = map′ (cong name) name-injective (x Name.≟ x₁) -name x ≟ meta x₁ = no (λ ()) -meta x ≟ nat x₁ = no (λ ()) -meta x ≟ word64 x₁ = no (λ ()) -meta x ≟ float x₁ = no (λ ()) -meta x ≟ char x₁ = no (λ ()) -meta x ≟ string x₁ = no (λ ()) -meta x ≟ name x₁ = no (λ ()) -meta x ≟ meta x₁ = map′ (cong meta) meta-injective (x Meta.≟ x₁) +infix 4 _≡?_ +_≡?_ : DecidableEquality Literal +nat x ≡? nat x₁ = map′ (cong nat) nat-injective (x ℕ.≡? x₁) +nat x ≡? word64 x₁ = no (λ ()) +nat x ≡? float x₁ = no (λ ()) +nat x ≡? char x₁ = no (λ ()) +nat x ≡? string x₁ = no (λ ()) +nat x ≡? name x₁ = no (λ ()) +nat x ≡? meta x₁ = no (λ ()) +word64 x ≡? word64 x₁ = map′ (cong word64) word64-injective (x Word64.≡? x₁) +word64 x ≡? nat x₁ = no (λ ()) +word64 x ≡? float x₁ = no (λ ()) +word64 x ≡? char x₁ = no (λ ()) +word64 x ≡? string x₁ = no (λ ()) +word64 x ≡? name x₁ = no (λ ()) +word64 x ≡? meta x₁ = no (λ ()) +float x ≡? nat x₁ = no (λ ()) +float x ≡? word64 x₁ = no (λ ()) +float x ≡? float x₁ = map′ (cong float) float-injective (x Float.≡? x₁) +float x ≡? char x₁ = no (λ ()) +float x ≡? string x₁ = no (λ ()) +float x ≡? name x₁ = no (λ ()) +float x ≡? meta x₁ = no (λ ()) +char x ≡? nat x₁ = no (λ ()) +char x ≡? word64 x₁ = no (λ ()) +char x ≡? float x₁ = no (λ ()) +char x ≡? char x₁ = map′ (cong char) char-injective (x Char.≡? x₁) +char x ≡? string x₁ = no (λ ()) +char x ≡? name x₁ = no (λ ()) +char x ≡? meta x₁ = no (λ ()) +string x ≡? nat x₁ = no (λ ()) +string x ≡? word64 x₁ = no (λ ()) +string x ≡? float x₁ = no (λ ()) +string x ≡? char x₁ = no (λ ()) +string x ≡? string x₁ = map′ (cong string) string-injective (x String.≡? x₁) +string x ≡? name x₁ = no (λ ()) +string x ≡? meta x₁ = no (λ ()) +name x ≡? nat x₁ = no (λ ()) +name x ≡? word64 x₁ = no (λ ()) +name x ≡? float x₁ = no (λ ()) +name x ≡? char x₁ = no (λ ()) +name x ≡? string x₁ = no (λ ()) +name x ≡? name x₁ = map′ (cong name) name-injective (x Name.≡? x₁) +name x ≡? meta x₁ = no (λ ()) +meta x ≡? nat x₁ = no (λ ()) +meta x ≡? word64 x₁ = no (λ ()) +meta x ≡? float x₁ = no (λ ()) +meta x ≡? char x₁ = no (λ ()) +meta x ≡? string x₁ = no (λ ()) +meta x ≡? name x₁ = no (λ ()) +meta x ≡? meta x₁ = map′ (cong meta) meta-injective (x Meta.≡? x₁) infix 4 _≡ᵇ_ _≡ᵇ_ : Literal → Literal → Bool -l ≡ᵇ l′ = isYes (l ≟ l′) +l ≡ᵇ l′ = isYes (l ≡? l′) + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda index bef152149f..4aaa009fa1 100644 --- a/src/Reflection/AST/Meta.agda +++ b/src/Reflection/AST/Meta.agda @@ -8,7 +8,7 @@ module Reflection.AST.Meta where -import Data.Nat.Properties as ℕ using (_≟_) +import Data.Nat.Properties as ℕ using (_≡?_) open import Function.Base using (_on_) open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) @@ -24,13 +24,29 @@ open import Agda.Builtin.Reflection.Properties public -- Equality of metas is decidable. -infix 4 _≈?_ _≟_ _≈_ +infix 4 _≈?_ _≡?_ _≈_ _≈_ : Rel Meta _ _≈_ = _≡_ on toℕ _≈?_ : Decidable _≈_ -_≈?_ = On.decidable toℕ _≡_ ℕ._≟_ +_≈?_ = On.decidable toℕ _≡_ ℕ._≡?_ -_≟_ : DecidableEquality Meta -m ≟ n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n) +_≡?_ : DecidableEquality Meta +m ≡? n = map′ (toℕ-injective _ _) (cong toℕ) (m ≈? n) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda index 867d14bd6e..055d5df0d1 100644 --- a/src/Reflection/AST/Name.agda +++ b/src/Reflection/AST/Name.agda @@ -10,7 +10,7 @@ module Reflection.AST.Name where open import Data.List.Base using (List) import Data.Product.Properties as Prodₚ using (≡-dec) -import Data.Word64.Properties as Wₚ using (_≟_) +import Data.Word64.Properties as Wₚ using (_≡?_) open import Function.Base using (_on_) open import Relation.Nullary.Decidable.Core using (map′) open import Relation.Binary.Core using (Rel) @@ -38,13 +38,29 @@ Names = List Name -- Decidable equality for names ------------------------------------------------------------------------ -infix 4 _≈?_ _≟_ _≈_ +infix 4 _≈?_ _≡?_ _≈_ _≈_ : Rel Name _ _≈_ = _≡_ on toWords _≈?_ : Decidable _≈_ -_≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≟_ Wₚ._≟_) +_≈?_ = decidable toWords _≡_ (Prodₚ.≡-dec Wₚ._≡?_ Wₚ._≡?_) -_≟_ : DecidableEquality Name -m ≟ n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n) +_≡?_ : DecidableEquality Name +m ≡? n = map′ (toWords-injective _ _) (cong toWords) (m ≈? n) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟_ +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} diff --git a/src/Reflection/AST/Pattern.agda b/src/Reflection/AST/Pattern.agda index 814baf1038..ea8e41899f 100644 --- a/src/Reflection/AST/Pattern.agda +++ b/src/Reflection/AST/Pattern.agda @@ -24,6 +24,6 @@ open import Reflection.AST.Term public ; pat-con-injective to con-injective ; pat-var-injective to var-injective ; pat-lit-injective to lit-injective - ; _≟-Patterns_ to _≟s_ - ; _≟-Pattern_ to _≟_ + ; _≡?-Patterns_ to _≟s_ + ; _≡?-Pattern_ to _≡?_ ) diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda index 0a1b9e3b53..9a3dc369b5 100644 --- a/src/Reflection/AST/Term.agda +++ b/src/Reflection/AST/Term.agda @@ -11,21 +11,21 @@ module Reflection.AST.Term where open import Data.List.Base as List hiding (_++_) open import Data.List.Properties using (∷-dec) open import Data.Nat.Base using (ℕ; zero; suc) -import Data.Nat.Properties as ℕ using (_≟_) +import Data.Nat.Properties as ℕ using (_≡?_) open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁) open import Data.Product.Properties using (,-injective) open import Data.Maybe.Base using (Maybe; just; nothing) open import Data.String.Base using (String) -open import Data.String.Properties as String hiding (_≟_) +open import Data.String.Properties as String hiding (_≟_; _≡?_) open import Relation.Nullary.Decidable using (map′; _×?_; yes; no) open import Relation.Binary.Definitions using (Decidable; DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂) open import Reflection.AST.Abstraction using (Abs; abs; unAbs-dec) open import Reflection.AST.Argument as Arg open import Reflection.AST.Argument.Information using (visibility) -open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_) -import Reflection.AST.Literal as Literal using (Literal; _≟_) -import Reflection.AST.Meta as Meta using (Meta; _≟_) +open import Reflection.AST.Argument.Visibility as Visibility hiding (_≟_; _≡?_) +import Reflection.AST.Literal as Literal using (Literal; _≡?_) +import Reflection.AST.Meta as Meta using (Meta; _≡?_) open import Reflection.AST.Name as Name using (Name) ------------------------------------------------------------------------ @@ -127,60 +127,60 @@ absurd-clause-injective₂ refl = refl absurd-clause-injective : ∀ {tel tel′ ps ps′} → absurd-clause tel ps ≡ absurd-clause tel′ ps′ → tel ≡ tel′ × ps ≡ ps′ absurd-clause-injective = < absurd-clause-injective₁ , absurd-clause-injective₂ > -infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ - _≟-Clause_ _≟-Clauses_ _≟_ - _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_ - -_≟-AbsTerm_ : DecidableEquality (Abs Term) -_≟-AbsType_ : DecidableEquality (Abs Type) -_≟-ArgTerm_ : DecidableEquality (Arg Term) -_≟-ArgType_ : DecidableEquality (Arg Type) -_≟-Args_ : DecidableEquality (Args Term) -_≟-Clause_ : DecidableEquality Clause -_≟-Clauses_ : DecidableEquality Clauses -_≟_ : DecidableEquality Term -_≟-Sort_ : DecidableEquality Sort -_≟-Patterns_ : DecidableEquality (Args Pattern) -_≟-Pattern_ : DecidableEquality Pattern +infix 4 _≡?-AbsTerm_ _≡?-AbsType_ _≡?-ArgTerm_ _≡?-ArgType_ _≡?-Args_ + _≡?-Clause_ _≡?-Clauses_ _≡?_ + _≡?-Sort_ _≡?-Pattern_ _≡?-Patterns_ _≡?-Telescope_ + +_≡?-AbsTerm_ : DecidableEquality (Abs Term) +_≡?-AbsType_ : DecidableEquality (Abs Type) +_≡?-ArgTerm_ : DecidableEquality (Arg Term) +_≡?-ArgType_ : DecidableEquality (Arg Type) +_≡?-Args_ : DecidableEquality (Args Term) +_≡?-Clause_ : DecidableEquality Clause +_≡?-Clauses_ : DecidableEquality Clauses +_≡?_ : DecidableEquality Term +_≡?-Sort_ : DecidableEquality Sort +_≡?-Patterns_ : DecidableEquality (Args Pattern) +_≡?-Pattern_ : DecidableEquality Pattern -- Decidable equality 'transformers' -- We need to inline these because the terms are not sized so -- termination would not obvious if we were to use higher-order -- functions such as Data.List.Properties' ≡-dec -abs s a ≟-AbsTerm abs s′ a′ = unAbs-dec (a ≟ a′) -abs s a ≟-AbsType abs s′ a′ = unAbs-dec (a ≟ a′) -arg i a ≟-ArgTerm arg i′ a′ = unArg-dec (a ≟ a′) -arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′) - -[] ≟-Args [] = yes refl -(x ∷ xs) ≟-Args (y ∷ ys) = ∷-dec (x ≟-ArgTerm y) (xs ≟-Args ys) -[] ≟-Args (_ ∷ _) = no λ() -(_ ∷ _) ≟-Args [] = no λ() - -[] ≟-Clauses [] = yes refl -(x ∷ xs) ≟-Clauses (y ∷ ys) = ∷-dec (x ≟-Clause y) (xs ≟-Clauses ys) -[] ≟-Clauses (_ ∷ _) = no λ() -(_ ∷ _) ≟-Clauses [] = no λ() - -_≟-Telescope_ : DecidableEquality Telescope -[] ≟-Telescope [] = yes refl -((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = ∷-dec - (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≟ x′) ×? (t ≟-ArgTerm t′))) - (tel ≟-Telescope tel′) -[] ≟-Telescope (_ ∷ _) = no λ () -(_ ∷ _) ≟-Telescope [] = no λ () - -clause tel ps b ≟-Clause clause tel′ ps′ b′ = +abs s a ≡?-AbsTerm abs s′ a′ = unAbs-dec (a ≡? a′) +abs s a ≡?-AbsType abs s′ a′ = unAbs-dec (a ≡? a′) +arg i a ≡?-ArgTerm arg i′ a′ = unArg-dec (a ≡? a′) +arg i a ≡?-ArgType arg i′ a′ = unArg-dec (a ≡? a′) + +[] ≡?-Args [] = yes refl +(x ∷ xs) ≡?-Args (y ∷ ys) = ∷-dec (x ≡?-ArgTerm y) (xs ≡?-Args ys) +[] ≡?-Args (_ ∷ _) = no λ() +(_ ∷ _) ≡?-Args [] = no λ() + +[] ≡?-Clauses [] = yes refl +(x ∷ xs) ≡?-Clauses (y ∷ ys) = ∷-dec (x ≡?-Clause y) (xs ≡?-Clauses ys) +[] ≡?-Clauses (_ ∷ _) = no λ() +(_ ∷ _) ≡?-Clauses [] = no λ() + +_≡?-Telescope_ : DecidableEquality Telescope +[] ≡?-Telescope [] = yes refl +((x , t) ∷ tel) ≡?-Telescope ((x′ , t′) ∷ tel′) = ∷-dec + (map′ (uncurry (cong₂ _,_)) ,-injective ((x String.≡? x′) ×? (t ≡?-ArgTerm t′))) + (tel ≡?-Telescope tel′) +[] ≡?-Telescope (_ ∷ _) = no λ () +(_ ∷ _) ≡?-Telescope [] = no λ () + +clause tel ps b ≡?-Clause clause tel′ ps′ b′ = map′ (λ (tel≡tel′ , ps≡ps′ , b≡b′) → cong₂ (uncurry clause) (cong₂ _,_ tel≡tel′ ps≡ps′) b≡b′) clause-injective - (tel ≟-Telescope tel′ ×? ps ≟-Patterns ps′ ×? b ≟ b′) -absurd-clause tel ps ≟-Clause absurd-clause tel′ ps′ = + (tel ≡?-Telescope tel′ ×? ps ≡?-Patterns ps′ ×? b ≡? b′) +absurd-clause tel ps ≡?-Clause absurd-clause tel′ ps′ = map′ (uncurry (cong₂ absurd-clause)) absurd-clause-injective - (tel ≟-Telescope tel′ ×? ps ≟-Patterns ps′) -clause _ _ _ ≟-Clause absurd-clause _ _ = no λ() -absurd-clause _ _ ≟-Clause clause _ _ _ = no λ() + (tel ≡?-Telescope tel′ ×? ps ≡?-Patterns ps′) +clause _ _ _ ≡?-Clause absurd-clause _ _ = no λ() +absurd-clause _ _ ≡?-Clause clause _ _ _ = no λ() var-injective₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′ var-injective₁ refl = refl @@ -266,151 +266,151 @@ propLit-injective refl = refl inf-injective : ∀ {x y} → inf x ≡ inf y → x ≡ y inf-injective refl = refl -var x args ≟ var x′ args′ = - map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×? args ≟-Args args′) -con c args ≟ con c′ args′ = - map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×? args ≟-Args args′) -def f args ≟ def f′ args′ = - map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×? args ≟-Args args′) -meta x args ≟ meta x′ args′ = - map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′ ×? args ≟-Args args′) -lam v t ≟ lam v′ t′ = - map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×? t ≟-AbsTerm t′) -pat-lam cs args ≟ pat-lam cs′ args′ = - map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×? args ≟-Args args′) -pi t₁ t₂ ≟ pi t₁′ t₂′ = - map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≟-ArgType t₁′ ×? t₂ ≟-AbsType t₂′) -sort s ≟ sort s′ = map′ (cong sort) sort-injective (s ≟-Sort s′) -lit l ≟ lit l′ = map′ (cong lit) lit-injective (l Literal.≟ l′) -unknown ≟ unknown = yes refl - -var x args ≟ con c args′ = no λ() -var x args ≟ def f args′ = no λ() -var x args ≟ lam v t = no λ() -var x args ≟ pi t₁ t₂ = no λ() -var x args ≟ sort _ = no λ() -var x args ≟ lit _ = no λ() -var x args ≟ meta _ _ = no λ() -var x args ≟ unknown = no λ() -con c args ≟ var x args′ = no λ() -con c args ≟ def f args′ = no λ() -con c args ≟ lam v t = no λ() -con c args ≟ pi t₁ t₂ = no λ() -con c args ≟ sort _ = no λ() -con c args ≟ lit _ = no λ() -con c args ≟ meta _ _ = no λ() -con c args ≟ unknown = no λ() -def f args ≟ var x args′ = no λ() -def f args ≟ con c args′ = no λ() -def f args ≟ lam v t = no λ() -def f args ≟ pi t₁ t₂ = no λ() -def f args ≟ sort _ = no λ() -def f args ≟ lit _ = no λ() -def f args ≟ meta _ _ = no λ() -def f args ≟ unknown = no λ() -lam v t ≟ var x args = no λ() -lam v t ≟ con c args = no λ() -lam v t ≟ def f args = no λ() -lam v t ≟ pi t₁ t₂ = no λ() -lam v t ≟ sort _ = no λ() -lam v t ≟ lit _ = no λ() -lam v t ≟ meta _ _ = no λ() -lam v t ≟ unknown = no λ() -pi t₁ t₂ ≟ var x args = no λ() -pi t₁ t₂ ≟ con c args = no λ() -pi t₁ t₂ ≟ def f args = no λ() -pi t₁ t₂ ≟ lam v t = no λ() -pi t₁ t₂ ≟ sort _ = no λ() -pi t₁ t₂ ≟ lit _ = no λ() -pi t₁ t₂ ≟ meta _ _ = no λ() -pi t₁ t₂ ≟ unknown = no λ() -sort _ ≟ var x args = no λ() -sort _ ≟ con c args = no λ() -sort _ ≟ def f args = no λ() -sort _ ≟ lam v t = no λ() -sort _ ≟ pi t₁ t₂ = no λ() -sort _ ≟ lit _ = no λ() -sort _ ≟ meta _ _ = no λ() -sort _ ≟ unknown = no λ() -lit _ ≟ var x args = no λ() -lit _ ≟ con c args = no λ() -lit _ ≟ def f args = no λ() -lit _ ≟ lam v t = no λ() -lit _ ≟ pi t₁ t₂ = no λ() -lit _ ≟ sort _ = no λ() -lit _ ≟ meta _ _ = no λ() -lit _ ≟ unknown = no λ() -meta _ _ ≟ var x args = no λ() -meta _ _ ≟ con c args = no λ() -meta _ _ ≟ def f args = no λ() -meta _ _ ≟ lam v t = no λ() -meta _ _ ≟ pi t₁ t₂ = no λ() -meta _ _ ≟ sort _ = no λ() -meta _ _ ≟ lit _ = no λ() -meta _ _ ≟ unknown = no λ() -unknown ≟ var x args = no λ() -unknown ≟ con c args = no λ() -unknown ≟ def f args = no λ() -unknown ≟ lam v t = no λ() -unknown ≟ pi t₁ t₂ = no λ() -unknown ≟ sort _ = no λ() -unknown ≟ lit _ = no λ() -unknown ≟ meta _ _ = no λ() -pat-lam _ _ ≟ var x args = no λ() -pat-lam _ _ ≟ con c args = no λ() -pat-lam _ _ ≟ def f args = no λ() -pat-lam _ _ ≟ lam v t = no λ() -pat-lam _ _ ≟ pi t₁ t₂ = no λ() -pat-lam _ _ ≟ sort _ = no λ() -pat-lam _ _ ≟ lit _ = no λ() -pat-lam _ _ ≟ meta _ _ = no λ() -pat-lam _ _ ≟ unknown = no λ() -var x args ≟ pat-lam _ _ = no λ() -con c args ≟ pat-lam _ _ = no λ() -def f args ≟ pat-lam _ _ = no λ() -lam v t ≟ pat-lam _ _ = no λ() -pi t₁ t₂ ≟ pat-lam _ _ = no λ() -sort _ ≟ pat-lam _ _ = no λ() -lit _ ≟ pat-lam _ _ = no λ() -meta _ _ ≟ pat-lam _ _ = no λ() -unknown ≟ pat-lam _ _ = no λ() - -set t ≟-Sort set t′ = map′ (cong set) set-injective (t ≟ t′) -lit n ≟-Sort lit n′ = map′ (cong lit) slit-injective (n ℕ.≟ n′) -prop t ≟-Sort prop t′ = map′ (cong prop) prop-injective (t ≟ t′) -propLit n ≟-Sort propLit n′ = map′ (cong propLit) propLit-injective (n ℕ.≟ n′) -inf n ≟-Sort inf n′ = map′ (cong inf) inf-injective (n ℕ.≟ n′) -unknown ≟-Sort unknown = yes refl -set _ ≟-Sort lit _ = no λ() -set _ ≟-Sort prop _ = no λ() -set _ ≟-Sort propLit _ = no λ() -set _ ≟-Sort inf _ = no λ() -set _ ≟-Sort unknown = no λ() -lit _ ≟-Sort set _ = no λ() -lit _ ≟-Sort prop _ = no λ() -lit _ ≟-Sort propLit _ = no λ() -lit _ ≟-Sort inf _ = no λ() -lit _ ≟-Sort unknown = no λ() -prop _ ≟-Sort set _ = no λ() -prop _ ≟-Sort lit _ = no λ() -prop _ ≟-Sort propLit _ = no λ() -prop _ ≟-Sort inf _ = no λ() -prop _ ≟-Sort unknown = no λ() -propLit _ ≟-Sort set _ = no λ() -propLit _ ≟-Sort lit _ = no λ() -propLit _ ≟-Sort prop _ = no λ() -propLit _ ≟-Sort inf _ = no λ() -propLit _ ≟-Sort unknown = no λ() -inf _ ≟-Sort set _ = no λ() -inf _ ≟-Sort lit _ = no λ() -inf _ ≟-Sort prop _ = no λ() -inf _ ≟-Sort propLit _ = no λ() -inf _ ≟-Sort unknown = no λ() -unknown ≟-Sort set _ = no λ() -unknown ≟-Sort lit _ = no λ() -unknown ≟-Sort prop _ = no λ() -unknown ≟-Sort propLit _ = no λ() -unknown ≟-Sort inf _ = no λ() +var x args ≡? var x′ args′ = + map′ (uncurry (cong₂ var)) var-injective (x ℕ.≡? x′ ×? args ≡?-Args args′) +con c args ≡? con c′ args′ = + map′ (uncurry (cong₂ con)) con-injective (c Name.≡? c′ ×? args ≡?-Args args′) +def f args ≡? def f′ args′ = + map′ (uncurry (cong₂ def)) def-injective (f Name.≡? f′ ×? args ≡?-Args args′) +meta x args ≡? meta x′ args′ = + map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≡? x′ ×? args ≡?-Args args′) +lam v t ≡? lam v′ t′ = + map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≡? v′ ×? t ≡?-AbsTerm t′) +pat-lam cs args ≡? pat-lam cs′ args′ = + map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≡?-Clauses cs′ ×? args ≡?-Args args′) +pi t₁ t₂ ≡? pi t₁′ t₂′ = + map′ (uncurry (cong₂ pi)) pi-injective (t₁ ≡?-ArgType t₁′ ×? t₂ ≡?-AbsType t₂′) +sort s ≡? sort s′ = map′ (cong sort) sort-injective (s ≡?-Sort s′) +lit l ≡? lit l′ = map′ (cong lit) lit-injective (l Literal.≡? l′) +unknown ≡? unknown = yes refl + +var x args ≡? con c args′ = no λ() +var x args ≡? def f args′ = no λ() +var x args ≡? lam v t = no λ() +var x args ≡? pi t₁ t₂ = no λ() +var x args ≡? sort _ = no λ() +var x args ≡? lit _ = no λ() +var x args ≡? meta _ _ = no λ() +var x args ≡? unknown = no λ() +con c args ≡? var x args′ = no λ() +con c args ≡? def f args′ = no λ() +con c args ≡? lam v t = no λ() +con c args ≡? pi t₁ t₂ = no λ() +con c args ≡? sort _ = no λ() +con c args ≡? lit _ = no λ() +con c args ≡? meta _ _ = no λ() +con c args ≡? unknown = no λ() +def f args ≡? var x args′ = no λ() +def f args ≡? con c args′ = no λ() +def f args ≡? lam v t = no λ() +def f args ≡? pi t₁ t₂ = no λ() +def f args ≡? sort _ = no λ() +def f args ≡? lit _ = no λ() +def f args ≡? meta _ _ = no λ() +def f args ≡? unknown = no λ() +lam v t ≡? var x args = no λ() +lam v t ≡? con c args = no λ() +lam v t ≡? def f args = no λ() +lam v t ≡? pi t₁ t₂ = no λ() +lam v t ≡? sort _ = no λ() +lam v t ≡? lit _ = no λ() +lam v t ≡? meta _ _ = no λ() +lam v t ≡? unknown = no λ() +pi t₁ t₂ ≡? var x args = no λ() +pi t₁ t₂ ≡? con c args = no λ() +pi t₁ t₂ ≡? def f args = no λ() +pi t₁ t₂ ≡? lam v t = no λ() +pi t₁ t₂ ≡? sort _ = no λ() +pi t₁ t₂ ≡? lit _ = no λ() +pi t₁ t₂ ≡? meta _ _ = no λ() +pi t₁ t₂ ≡? unknown = no λ() +sort _ ≡? var x args = no λ() +sort _ ≡? con c args = no λ() +sort _ ≡? def f args = no λ() +sort _ ≡? lam v t = no λ() +sort _ ≡? pi t₁ t₂ = no λ() +sort _ ≡? lit _ = no λ() +sort _ ≡? meta _ _ = no λ() +sort _ ≡? unknown = no λ() +lit _ ≡? var x args = no λ() +lit _ ≡? con c args = no λ() +lit _ ≡? def f args = no λ() +lit _ ≡? lam v t = no λ() +lit _ ≡? pi t₁ t₂ = no λ() +lit _ ≡? sort _ = no λ() +lit _ ≡? meta _ _ = no λ() +lit _ ≡? unknown = no λ() +meta _ _ ≡? var x args = no λ() +meta _ _ ≡? con c args = no λ() +meta _ _ ≡? def f args = no λ() +meta _ _ ≡? lam v t = no λ() +meta _ _ ≡? pi t₁ t₂ = no λ() +meta _ _ ≡? sort _ = no λ() +meta _ _ ≡? lit _ = no λ() +meta _ _ ≡? unknown = no λ() +unknown ≡? var x args = no λ() +unknown ≡? con c args = no λ() +unknown ≡? def f args = no λ() +unknown ≡? lam v t = no λ() +unknown ≡? pi t₁ t₂ = no λ() +unknown ≡? sort _ = no λ() +unknown ≡? lit _ = no λ() +unknown ≡? meta _ _ = no λ() +pat-lam _ _ ≡? var x args = no λ() +pat-lam _ _ ≡? con c args = no λ() +pat-lam _ _ ≡? def f args = no λ() +pat-lam _ _ ≡? lam v t = no λ() +pat-lam _ _ ≡? pi t₁ t₂ = no λ() +pat-lam _ _ ≡? sort _ = no λ() +pat-lam _ _ ≡? lit _ = no λ() +pat-lam _ _ ≡? meta _ _ = no λ() +pat-lam _ _ ≡? unknown = no λ() +var x args ≡? pat-lam _ _ = no λ() +con c args ≡? pat-lam _ _ = no λ() +def f args ≡? pat-lam _ _ = no λ() +lam v t ≡? pat-lam _ _ = no λ() +pi t₁ t₂ ≡? pat-lam _ _ = no λ() +sort _ ≡? pat-lam _ _ = no λ() +lit _ ≡? pat-lam _ _ = no λ() +meta _ _ ≡? pat-lam _ _ = no λ() +unknown ≡? pat-lam _ _ = no λ() + +set t ≡?-Sort set t′ = map′ (cong set) set-injective (t ≡? t′) +lit n ≡?-Sort lit n′ = map′ (cong lit) slit-injective (n ℕ.≡? n′) +prop t ≡?-Sort prop t′ = map′ (cong prop) prop-injective (t ≡? t′) +propLit n ≡?-Sort propLit n′ = map′ (cong propLit) propLit-injective (n ℕ.≡? n′) +inf n ≡?-Sort inf n′ = map′ (cong inf) inf-injective (n ℕ.≡? n′) +unknown ≡?-Sort unknown = yes refl +set _ ≡?-Sort lit _ = no λ() +set _ ≡?-Sort prop _ = no λ() +set _ ≡?-Sort propLit _ = no λ() +set _ ≡?-Sort inf _ = no λ() +set _ ≡?-Sort unknown = no λ() +lit _ ≡?-Sort set _ = no λ() +lit _ ≡?-Sort prop _ = no λ() +lit _ ≡?-Sort propLit _ = no λ() +lit _ ≡?-Sort inf _ = no λ() +lit _ ≡?-Sort unknown = no λ() +prop _ ≡?-Sort set _ = no λ() +prop _ ≡?-Sort lit _ = no λ() +prop _ ≡?-Sort propLit _ = no λ() +prop _ ≡?-Sort inf _ = no λ() +prop _ ≡?-Sort unknown = no λ() +propLit _ ≡?-Sort set _ = no λ() +propLit _ ≡?-Sort lit _ = no λ() +propLit _ ≡?-Sort prop _ = no λ() +propLit _ ≡?-Sort inf _ = no λ() +propLit _ ≡?-Sort unknown = no λ() +inf _ ≡?-Sort set _ = no λ() +inf _ ≡?-Sort lit _ = no λ() +inf _ ≡?-Sort prop _ = no λ() +inf _ ≡?-Sort propLit _ = no λ() +inf _ ≡?-Sort unknown = no λ() +unknown ≡?-Sort set _ = no λ() +unknown ≡?-Sort lit _ = no λ() +unknown ≡?-Sort prop _ = no λ() +unknown ≡?-Sort propLit _ = no λ() +unknown ≡?-Sort inf _ = no λ() pat-con-injective₁ : ∀ {c c′ args args′} → Pattern.con c args ≡ con c′ args′ → c ≡ c′ @@ -437,46 +437,120 @@ dot-injective refl = refl absurd-injective : ∀ {x y} → absurd x ≡ absurd y → x ≡ y absurd-injective refl = refl -con c ps ≟-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≟ c′ ×? ps ≟-Patterns ps′) -var x ≟-Pattern var x′ = map′ (cong var) pat-var-injective (x ℕ.≟ x′) -lit l ≟-Pattern lit l′ = map′ (cong lit) pat-lit-injective (l Literal.≟ l′) -proj a ≟-Pattern proj a′ = map′ (cong proj) proj-injective (a Name.≟ a′) -dot t ≟-Pattern dot t′ = map′ (cong dot) dot-injective (t ≟ t′) -absurd x ≟-Pattern absurd x′ = map′ (cong absurd) absurd-injective (x ℕ.≟ x′) - -con x x₁ ≟-Pattern dot x₂ = no (λ ()) -con x x₁ ≟-Pattern var x₂ = no (λ ()) -con x x₁ ≟-Pattern lit x₂ = no (λ ()) -con x x₁ ≟-Pattern proj x₂ = no (λ ()) -con x x₁ ≟-Pattern absurd x₂ = no (λ ()) -dot x ≟-Pattern con x₁ x₂ = no (λ ()) -dot x ≟-Pattern var x₁ = no (λ ()) -dot x ≟-Pattern lit x₁ = no (λ ()) -dot x ≟-Pattern proj x₁ = no (λ ()) -dot x ≟-Pattern absurd x₁ = no (λ ()) -var s ≟-Pattern con x x₁ = no (λ ()) -var s ≟-Pattern dot x = no (λ ()) -var s ≟-Pattern lit x = no (λ ()) -var s ≟-Pattern proj x = no (λ ()) -var s ≟-Pattern absurd x = no (λ ()) -lit x ≟-Pattern con x₁ x₂ = no (λ ()) -lit x ≟-Pattern dot x₁ = no (λ ()) -lit x ≟-Pattern var _ = no (λ ()) -lit x ≟-Pattern proj x₁ = no (λ ()) -lit x ≟-Pattern absurd x₁ = no (λ ()) -proj x ≟-Pattern con x₁ x₂ = no (λ ()) -proj x ≟-Pattern dot x₁ = no (λ ()) -proj x ≟-Pattern var _ = no (λ ()) -proj x ≟-Pattern lit x₁ = no (λ ()) -proj x ≟-Pattern absurd x₁ = no (λ ()) -absurd x ≟-Pattern con x₁ x₂ = no (λ ()) -absurd x ≟-Pattern dot x₁ = no (λ ()) -absurd x ≟-Pattern var _ = no (λ ()) -absurd x ≟-Pattern lit x₁ = no (λ ()) -absurd x ≟-Pattern proj x₁ = no (λ ()) - -[] ≟-Patterns [] = yes refl -(arg i p ∷ xs) ≟-Patterns (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≟-Pattern q)) (xs ≟-Patterns ys) - -[] ≟-Patterns (_ ∷ _) = no λ() -(_ ∷ _) ≟-Patterns [] = no λ() +con c ps ≡?-Pattern con c′ ps′ = map′ (uncurry (cong₂ con)) pat-con-injective (c Name.≡? c′ ×? ps ≡?-Patterns ps′) +var x ≡?-Pattern var x′ = map′ (cong var) pat-var-injective (x ℕ.≡? x′) +lit l ≡?-Pattern lit l′ = map′ (cong lit) pat-lit-injective (l Literal.≡? l′) +proj a ≡?-Pattern proj a′ = map′ (cong proj) proj-injective (a Name.≡? a′) +dot t ≡?-Pattern dot t′ = map′ (cong dot) dot-injective (t ≡? t′) +absurd x ≡?-Pattern absurd x′ = map′ (cong absurd) absurd-injective (x ℕ.≡? x′) + +con x x₁ ≡?-Pattern dot x₂ = no (λ ()) +con x x₁ ≡?-Pattern var x₂ = no (λ ()) +con x x₁ ≡?-Pattern lit x₂ = no (λ ()) +con x x₁ ≡?-Pattern proj x₂ = no (λ ()) +con x x₁ ≡?-Pattern absurd x₂ = no (λ ()) +dot x ≡?-Pattern con x₁ x₂ = no (λ ()) +dot x ≡?-Pattern var x₁ = no (λ ()) +dot x ≡?-Pattern lit x₁ = no (λ ()) +dot x ≡?-Pattern proj x₁ = no (λ ()) +dot x ≡?-Pattern absurd x₁ = no (λ ()) +var s ≡?-Pattern con x x₁ = no (λ ()) +var s ≡?-Pattern dot x = no (λ ()) +var s ≡?-Pattern lit x = no (λ ()) +var s ≡?-Pattern proj x = no (λ ()) +var s ≡?-Pattern absurd x = no (λ ()) +lit x ≡?-Pattern con x₁ x₂ = no (λ ()) +lit x ≡?-Pattern dot x₁ = no (λ ()) +lit x ≡?-Pattern var _ = no (λ ()) +lit x ≡?-Pattern proj x₁ = no (λ ()) +lit x ≡?-Pattern absurd x₁ = no (λ ()) +proj x ≡?-Pattern con x₁ x₂ = no (λ ()) +proj x ≡?-Pattern dot x₁ = no (λ ()) +proj x ≡?-Pattern var _ = no (λ ()) +proj x ≡?-Pattern lit x₁ = no (λ ()) +proj x ≡?-Pattern absurd x₁ = no (λ ()) +absurd x ≡?-Pattern con x₁ x₂ = no (λ ()) +absurd x ≡?-Pattern dot x₁ = no (λ ()) +absurd x ≡?-Pattern var _ = no (λ ()) +absurd x ≡?-Pattern lit x₁ = no (λ ()) +absurd x ≡?-Pattern proj x₁ = no (λ ()) + +[] ≡?-Patterns [] = yes refl +(arg i p ∷ xs) ≡?-Patterns (arg j q ∷ ys) = ∷-dec (unArg-dec (p ≡?-Pattern q)) (xs ≡?-Patterns ys) + +[] ≡?-Patterns (_ ∷ _) = no λ() +(_ ∷ _) ≡?-Patterns [] = no λ() + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_ + _≟-Clause_ _≟-Clauses_ _≟_ + _≟-Sort_ _≟-Pattern_ _≟-Patterns_ _≟-Telescope_ + +_≟_ = _≡?_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟_ was deprecated in v2.4. +Please use _≡?_ instead." +#-} +_≟-AbsTerm_ = _≡?-AbsTerm_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟-AbsTerm_ was deprecated in v2.4. +Please use _≡?-AbsTerm_ instead." +#-} +_≟-AbsType_ = _≡?-AbsType_ +{-# WARNING_ON_USAGE _≟-AbsType_ +"Warning: _≟-AbsType_ was deprecated in v2.4. +Please use _≡?-AbsType_ instead." +#-} +_≟-ArgTerm_ = _≡?-ArgTerm_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟-ArgTerm_ was deprecated in v2.4. +Please use _≡?-ArgTerm_ instead." +#-} +_≟-ArgType_ = _≡?-ArgType_ +{-# WARNING_ON_USAGE _≟-ArgType_ +"Warning: _≟-ArgType_ was deprecated in v2.4. +Please use _≡?-ArgType_ instead." +#-} +_≟-Args_ = _≡?-Args_ +{-# WARNING_ON_USAGE _≟-Args_ +"Warning: _≟-Args_ was deprecated in v2.4. +Please use _≡?-Args_ instead." +#-} +_≟-Clause_ = _≡?-Clause_ +{-# WARNING_ON_USAGE _≟-Clause_ +"Warning: _≟-Clause_ was deprecated in v2.4. +Please use _≡?-Clause_ instead." +#-} +_≟-Clauses_ = _≡?-Clauses_ +{-# WARNING_ON_USAGE _≟_ +"Warning: _≟-Clauses_ was deprecated in v2.4. +Please use _≡?-Clauses_ instead." +#-} +_≟-Sort_ = _≡?-Sort_ +{-# WARNING_ON_USAGE _≟-Sort_ +"Warning: _≟-Sort_ was deprecated in v2.4. +Please use _≡?-Sort_ instead." +#-} +_≟-Pattern_ = _≡?-Pattern_ +{-# WARNING_ON_USAGE _≟-Pattern_ +"Warning: _≟-Pattern_ was deprecated in v2.4. +Please use _≡?-Pattern_ instead." +#-} +_≟-Patterns_ = _≡?-Patterns_ +{-# WARNING_ON_USAGE _≟-Patterns_ +"Warning: _≟-Patterns_ was deprecated in v2.4. +Please use _≡?-Patterns_ instead." +#-} +_≟-Telescope_ = _≡?-Telescope_ +{-# WARNING_ON_USAGE _≟-Telescope_ +"Warning: _≟-Telescope_ was deprecated in v2.4. +Please use _≡?-Telescope_ instead." +#-} diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda index 3a2a5f3524..8b799779a5 100644 --- a/src/Relation/Binary/Construct/Flip/Ord.agda +++ b/src/Relation/Binary/Construct/Flip/Ord.agda @@ -101,7 +101,7 @@ isEquivalence {≈ = ≈} eq = record isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈) isDecEquivalence {≈ = ≈} dec = record { isEquivalence = isEquivalence Dec.isEquivalence - ; _≟_ = decidable ≈ Dec._≟_ + ; _≈?_ = decidable ≈ Dec._≈?_ } where module Dec = IsDecEquivalence dec isPreorder : IsPreorder ≈ ∼ → IsPreorder (flip ≈) (flip ∼) @@ -127,7 +127,7 @@ isTotalOrder {≈ = ≈} {≤ = ≤} O = record isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder (flip ≈) (flip ≤) isDecTotalOrder {≈ = ≈} {≤ = ≤} O = record { isTotalOrder = isTotalOrder O.isTotalOrder - ; _≟_ = decidable ≈ O._≟_ + ; _≈?_ = decidable ≈ O._≈?_ ; _≤?_ = decidable ≤ O._≤?_ } where module O = IsDecTotalOrder O diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 4f4eb561a7..e061a893d4 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -111,7 +111,7 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where isDecPartialOrder : IsDecPartialOrder (SymInterior R) R isDecPartialOrder = record { isPartialOrder = isPartialOrder - ; _≟_ = decidable R? + ; _≈?_ = decidable R? ; _≤?_ = R? } diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda index d974768350..3623097128 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda @@ -113,10 +113,10 @@ isPartialOrder semilattice = record isDecPartialOrder : IsSemilattice _∙_ → Decidable _≈_ → IsDecPartialOrder _≈_ _≤_ -isDecPartialOrder semilattice _≟_ = record +isDecPartialOrder semilattice _≈?_ = record { isPartialOrder = isPartialOrder semilattice - ; _≟_ = _≟_ - ; _≤?_ = dec _≟_ + ; _≈?_ = _≈?_ + ; _≤?_ = dec _≈?_ } isTotalOrder : IsSemilattice _∙_ → Selective _∙_ → IsTotalOrder _≈_ _≤_ @@ -128,10 +128,10 @@ isTotalOrder latt sel = record isDecTotalOrder : IsSemilattice _∙_ → Selective _∙_ → Decidable _≈_ → IsDecTotalOrder _≈_ _≤_ -isDecTotalOrder latt sel _≟_ = record +isDecTotalOrder latt sel _≈?_ = record { isTotalOrder = isTotalOrder latt sel - ; _≟_ = _≟_ - ; _≤?_ = dec _≟_ + ; _≈?_ = _≈?_ + ; _≤?_ = dec _≈?_ } ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda index c103cc7bab..8e94efe242 100644 --- a/src/Relation/Binary/Construct/StrictToNonStrict.agda +++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda @@ -145,7 +145,7 @@ isTotalOrder STO = record isDecTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsDecTotalOrder _≈_ _≤_ isDecTotalOrder STO = record { isTotalOrder = isTotalOrder STO - ; _≟_ = S._≟_ + ; _≈?_ = S._≈?_ ; _≤?_ = decidable′ S.compare } where module S = IsStrictTotalOrder STO diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda index 6761bea53a..1be883007c 100644 --- a/src/Relation/Binary/HeterogeneousEquality.agda +++ b/src/Relation/Binary/HeterogeneousEquality.agda @@ -198,7 +198,7 @@ decSetoid dec = record { _≈_ = λ x y → x ≅ y ; isDecEquivalence = record { isEquivalence = isEquivalence - ; _≟_ = dec + ; _≈?_ = dec } } diff --git a/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda b/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda index b3ad700105..39d2bf3d0d 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda @@ -37,7 +37,7 @@ isDecEquivalence : ∀ {_≈_ : IRel Aᵢ ℓ} → IsIndexedDecEquivalence Aᵢ (index : I) → IsDecEquivalence (_≈_ {index}) isDecEquivalence isEq index = record { isEquivalence = isEquivalence E.isEquivalenceᵢ index - ; _≟_ = E._≟ᵢ_ + ; _≈?_ = E._≈ᵢ?_ } where module E = IsIndexedDecEquivalence isEq isPreorder : ∀ {_≈_ : IRel Aᵢ ℓ₁} {_∼_ : IRel Aᵢ ℓ₂} → diff --git a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda index 48265dbef5..575f681d4b 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda @@ -69,13 +69,19 @@ record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where record IsIndexedDecEquivalence : Set (i ⊔ a ⊔ ℓ) where - infix 4 _≟ᵢ_ + infix 4 _≟ᵢ_ _≈ᵢ?_ field - _≟ᵢ_ : Decidable A _≈ᵢ_ + _≈ᵢ?_ : Decidable A _≈ᵢ_ isEquivalenceᵢ : IsIndexedEquivalence open IsIndexedEquivalence isEquivalenceᵢ public + _≟ᵢ_ = _≈ᵢ?_ + {-# WARNING_ON_USAGE _≟ᵢ_ + "Warning: _≟ᵢ_ was deprecated in v2.4. + Please use _≈ᵢ?_ instead." + #-} + ------------------------------------------------------------------------ -- Preorders diff --git a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda index 90ea114cb5..493b1d9896 100644 --- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda @@ -119,8 +119,8 @@ dualMeetSemilattice = record ... | no x∨y≉y = no (contraposition x≤y⇒x∨y≈y x∨y≉y) ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_ -≈-dec⇒isDecPartialOrder _≟_ = record +≈-dec⇒isDecPartialOrder _≈?_ = record { isPartialOrder = isPartialOrder - ; _≟_ = _≟_ - ; _≤?_ = ≈-dec⇒≤-dec _≟_ + ; _≈?_ = _≈?_ + ; _≤?_ = ≈-dec⇒≤-dec _≈?_ } diff --git a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda index e5b77d4092..875412ebf9 100644 --- a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda +++ b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda @@ -49,11 +49,11 @@ open J dualJoinSemilattice public -- If ≈ is decidable then so is ≤ ≈-dec⇒≤-dec : Decidable _≈_ → Decidable _≤_ -≈-dec⇒≤-dec _≟_ = flip (≈-dec⇒≥-dec _≟_) +≈-dec⇒≤-dec _≈?_ = flip (≈-dec⇒≥-dec _≈?_) ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_ -≈-dec⇒isDecPartialOrder _≟_ = record +≈-dec⇒isDecPartialOrder _≈?_ = record { isPartialOrder = isPartialOrder - ; _≟_ = _≟_ - ; _≤?_ = ≈-dec⇒≤-dec _≟_ + ; _≈?_ = _≈?_ + ; _≤?_ = ≈-dec⇒≤-dec _≈?_ } diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda index faa81dd372..82116420a8 100644 --- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda +++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda @@ -92,7 +92,7 @@ isTotalOrder O = record isDecTotalOrder : IsDecTotalOrder _≈₂_ _≲₂_ → IsDecTotalOrder _≈₁_ _≲₁_ isDecTotalOrder O = record { isTotalOrder = isTotalOrder O.isTotalOrder - ; _≟_ = EqM.dec O._≟_ + ; _≈?_ = EqM.dec O._≈?_ ; _≤?_ = dec O._≤?_ } where module O = IsDecTotalOrder O diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda index 693e6ebf80..1b4bbe3e36 100644 --- a/src/Relation/Binary/Morphism/RelMonomorphism.agda +++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda @@ -61,5 +61,5 @@ isEquivalence isEq = record isDecEquivalence : IsDecEquivalence _∼₂_ → IsDecEquivalence _∼₁_ isDecEquivalence isDecEq = record { isEquivalence = isEquivalence E.isEquivalence - ; _≟_ = dec E._≟_ + ; _≈?_ = dec E._≈?_ } where module E = IsDecEquivalence isDecEq diff --git a/src/Relation/Binary/TypeClasses.agda b/src/Relation/Binary/TypeClasses.agda index 48f0271f6a..a958d6f915 100644 --- a/src/Relation/Binary/TypeClasses.agda +++ b/src/Relation/Binary/TypeClasses.agda @@ -10,5 +10,5 @@ module Relation.Binary.TypeClasses where open import Relation.Binary.Structures using (IsDecEquivalence; IsDecTotalOrder) public -open IsDecEquivalence {{...}} using (_≟_) public +open IsDecEquivalence {{...}} using (_≈?_) public open IsDecTotalOrder {{...}} using (_≤?_) public diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index ceffe6587d..d7e6a14571 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -108,7 +108,7 @@ private term' ← term symTerm' ← symTerm -- Don't show the same term twice. - let symErr = case term' Term.≟ symTerm' of λ where + let symErr = case term' Term.≡? symTerm' of λ where (yes _) → [] (no _) → strErr "\n" ∷ termErr symTerm' ∷ [] typeError (strErr "cong! failed, tried:\n" ∷ termErr term' ∷ symErr) diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda index cc3198269c..1533f09752 100644 --- a/src/Test/Golden.agda +++ b/src/Test/Golden.agda @@ -92,7 +92,7 @@ open import Data.Nat.ListAction using (sum) import Data.Nat.Show as ℕ using (show) open import Data.Product.Base using (_×_; _,_) open import Data.String.Base as String using (String; lines; unlines; unwords; concat) -open import Data.String.Properties as String using (_≟_) +open import Data.String.Properties as String using (_≡?_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂) open import Data.Unit.Base using (⊤) @@ -183,7 +183,7 @@ options(exe ∷ rest) = mkOptions exe rest where inj₂ (mfp , opts) ← pure $ go rest nothing (initOptions exe) where inj₁ arg → pure (inj₁ (InvalidArgument arg)) term ← fromMaybe "" <$> lookupEnv "TERM" - let opts = if does (term ≟ "DUMB") + let opts = if does (term ≡? "DUMB") then record opts { colour = false } else opts just fp ← pure mfp @@ -221,7 +221,7 @@ runTest opts testPath = do else putStrLn (fileNotFound "expected") pure (inj₁ testPath) - let result = does (out String.≟ exp) + let result = does (out String.≡? exp) if result then printTiming (opts .timing) time @@ -354,7 +354,7 @@ filterTests : Options → List String → List String filterTests opts = case onlyNames opts of λ where [] → id xs → let names = List.map String.toList xs in - filter (λ n → any? (λ m → infix? Char._≟_ m (String.toList n)) names) + filter (λ n → any? (λ m → infix? Char._≡?_ m (String.toList n)) names) poolRunner : Options → TestPool → IO Summary poolRunner opts pool = do diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda index b384207d7f..ce76e26375 100644 --- a/src/Text/Regex/Properties.agda +++ b/src/Text/Regex/Properties.agda @@ -52,7 +52,7 @@ open import Text.Regex.Properties.Core preorder public infix 4 _∈ᴿ?_ _∉ᴿ?_ _∈?ε _∈?[_] _∈?[^_] _∈ᴿ?_ : Decidable _∈ᴿ_ -c ∈ᴿ? [ a ] = map′ [_] (λ where [ eq ] → eq) (c ≟ a) +c ∈ᴿ? [ a ] = map′ [_] (λ where [ eq ] → eq) (c ≈? a) c ∈ᴿ? (lb ─ ub) = map′ (uncurry _─_) (λ where (ge ─ le) → ge , le) $ (lb ≤? c) ×? (c ≤? ub) From f7dee08b1b142bb1acf0841d00630f840b72403b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 12:18:54 +0000 Subject: [PATCH 05/20] fix: whitespace --- src/Algebra/Solver/Monoid/Normal.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Solver/Monoid/Normal.agda b/src/Algebra/Solver/Monoid/Normal.agda index 2195eeafac..4554873b6e 100644 --- a/src/Algebra/Solver/Monoid/Normal.agda +++ b/src/Algebra/Solver/Monoid/Normal.agda @@ -99,7 +99,7 @@ correct (e₁ ⊕ e₂) ρ = begin infix 4 _≟_ -_≟_ = _≡?_ +_≟_ = _≡?_ {-# WARNING_ON_USAGE _≟_ "Warning: _≟_ was deprecated in v2.4. Please use _≡?_ instead." From 845628712b7d38f6ff604614640b0e1ba41e0cd3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 12:49:01 +0000 Subject: [PATCH 06/20] add: `style-guide` entry --- doc/style-guide.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/doc/style-guide.md b/doc/style-guide.md index cfecfbd699..9ded0f896f 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -586,6 +586,12 @@ word within a compound word is capitalized except for the first word. converse relations are systematically introduced, eg `≥` as `\ge` and `≱` as `\gen`. +* Decidable predicates and relations should typically be written as `R?`, + where `R` is the underlying property being asserted to be `Decidable`, + moreover typically sharing the same fixity and precedence as `R`: thus + - `_≡?_` (at `infix 4`) for `DecidableEquality` + - `_≈?_` for the fieldname of the general `IsDecEquivalence` + * Any exceptions to these conventions should be flagged on the GitHub `agda-stdlib` issue tracker in the usual way. From 412eb939bb7d17637426961a6f8e0f76c064d36e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 13:27:13 +0000 Subject: [PATCH 07/20] fix: `test/reflection/assumption` --- tests/reflection/assumption/Main.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/reflection/assumption/Main.agda b/tests/reflection/assumption/Main.agda index cf0d21b514..bdc397613a 100644 --- a/tests/reflection/assumption/Main.agda +++ b/tests/reflection/assumption/Main.agda @@ -13,7 +13,7 @@ open import Data.Unit.Base using (⊤) open import Function.Base using (case_of_; _$_) open import Reflection.TCM hiding (pure) open import Reflection.AST.Term -open import Reflection.AST.Literal hiding (_≟_) +open import Reflection.AST.Literal hiding (_≟_; _≡?_) open import Reflection.AST.Argument using (Arg; unArg; arg) open import Reflection.AST.DeBruijn open import Reflection.AST.Show @@ -44,7 +44,7 @@ searchEntry : ℕ → Type → List (String × Arg Type) → Maybe ℕ searchEntry n ty [] = nothing searchEntry n ty ((_ , e) ∷ es) = do ty ← strengthen ty - if does (ty ≟ unArg e) + if does (ty ≡? unArg e) then just n else searchEntry (suc n) ty es From 377d56ebb6b1c37a594d18967398839949fc20f5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 13:31:16 +0000 Subject: [PATCH 08/20] fix: `data/trie` plus exports from `Data.String` --- src/Data/String.agda | 2 +- tests/data/trie/Main.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/String.agda b/src/Data/String.agda index 9186c514d1..e5717fff09 100644 --- a/src/Data/String.agda +++ b/src/Data/String.agda @@ -27,7 +27,7 @@ open import Data.List.Membership.DecPropositional Char._≡?_ -- Re-export contents of base, and decidability of equality open import Data.String.Base public -open import Data.String.Properties using (_≈?_; _≡?_; _ Date: Wed, 25 Feb 2026 19:35:52 +0000 Subject: [PATCH 09/20] fix: renaming and deprecation for `Fin` and `Nat` --- CHANGELOG.md | 19 ++++++++++++++----- src/Data/Nat/Properties.agda | 19 +++++++++++-------- 2 files changed, 25 insertions(+), 13 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f83411bc22..ec0466e228 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -87,6 +87,15 @@ Deprecated names ```agda ¬∀⟶∃¬-smallest ↦ ¬∀⇒∃¬-smallest ¬∀⟶∃¬- ↦ ¬∀⇒∃¬ + _≟_ ↦ _≡?_ + inj⇒≟ ↦ inj⇒≡? + ``` + +* In `Data.Nat.Properties`: + ```agda + _≟_ ↦ _≡?_ + ≟-diag ↦ ≡?-≡ + ≟-≡ ↦ ≡?-≢ ``` * In `Data.Rational.Properties`: @@ -239,10 +248,10 @@ Additions to existing modules * In `Data.Fin.Properties`: ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ - ≟-≡ : (eq : i ≡ j) → (i ≟ j) ≡ yes eq - ≟-≡-refl : (i : Fin n) → (i ≟ i) ≡ yes refl - ≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j - inject-< : inject j < i + ≡?-≡ : (eq : i ≡ j) → (i ≡? j) ≡ yes eq + ≡?-≡-refl : (i : Fin n) → (i ≡? i) ≡ yes refl + ≡?-≢ : (i≢j : i ≢ j) → (i ≡? j) ≡ no i≢j + inject-< : inject j < i record Least⟨_⟩ (P : Pred (Fin n) p) : Set p where constructor least @@ -305,7 +314,7 @@ Additions to existing modules * In `Data.Nat.Properties`: ```agda - ≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n + ≡?-≡-refl : ∀ n → (n ≡? n) ≡ yes refl ∸-suc : .(m ≤ n) → suc n ∸ m ≡ suc (n ∸ m) ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m 2*suc[n]≡2+n+n : ∀ n → 2 * (suc n) ≡ 2 + (n + n) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 1ddc89e2d6..b0bc4d77c6 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -111,11 +111,14 @@ m ≡? n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) ≡-irrelevant : Irrelevant {A = ℕ} _≡_ ≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≡?_ -≡?-diag : (eq : m ≡ n) → (m ≡? n) ≡ yes eq -≡?-diag = ≡-≡?-identity _≡?_ +≡?-≡ : (eq : m ≡ n) → (m ≡? n) ≡ yes eq +≡?-≡ = ≡-≡?-identity _≡?_ -≡?-≡ : (m≢n : m ≢ n) → (m ≡? n) ≡ no m≢n -≡?-≡ = ≢-≡?-identity _≡?_ +≡?-≡-refl : ∀ n → (n ≡? n) ≡ yes refl +≡?-≡-refl _ = ≡?-≡ refl + +≡?-≢ : (m≢n : m ≢ n) → (m ≡? n) ≡ no m≢n +≡?-≢ = ≢-≡?-identity _≡?_ ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ}) ≡-isDecEquivalence = record @@ -2470,14 +2473,14 @@ _≟_ = _≡?_ Please use _≡?_ instead." #-} -≟-diag = ≡?-diag +≟-diag = ≡?-≡ {-# WARNING_ON_USAGE ≟-diag "Warning: ≟-diag was deprecated in v2.4. -Please use ≡?-diag instead." +Please use ≡?-≡ instead." #-} -≟-≡ = ≡?-≡ +≟-≡ = ≡?-≢ {-# WARNING_ON_USAGE ≟-≡ "Warning: ≟-≡ was deprecated in v2.4. -Please use ≡?-≡ instead." +Please use ≡?-≢ instead." #-} From ed8643672764340c27d46d5477cf3ece3777daa1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 19:45:43 +0000 Subject: [PATCH 10/20] fix: more deprecations --- CHANGELOG.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ec0466e228..eef65a4f16 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -108,6 +108,12 @@ Deprecated names truncate-irrelevant ↦ Relation.Binary.PropositionalEquality.Core.refl ``` +* In `Relation.Binary.PropositionalEquality`: + ```agda + ≡-≟-identity ↦ ≡-≡?-identity + ≢-≟-identity ↦ ≢-≡?-identity + ``` + * In `Relation.Nullary.Decidable.Core`: ```agda ⊤-dec ↦ ⊤? @@ -115,6 +121,7 @@ Deprecated names _×-dec_ ↦ _×?_ _⊎-dec_ ↦ _⊎?_ _→-dec_ ↦ _→?_ + ``` * In `Relation.Nullary.Negation`: ```agda From a6143ab2d3247e3a56719372bd6ecbd91c7390c6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 25 Feb 2026 20:54:52 +0000 Subject: [PATCH 11/20] fix: cosmetic renaming --- src/Axiom/UniquenessOfIdentityProofs.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda index 752b9c444d..cb1ec76231 100644 --- a/src/Axiom/UniquenessOfIdentityProofs.agda +++ b/src/Axiom/UniquenessOfIdentityProofs.agda @@ -66,14 +66,14 @@ module Constant⇒UIP -- function over proofs of equality which is constant: it returns the -- proof produced by the decision procedure. -module Decidable⇒UIP (_≟_ : DecidableEquality A) +module Decidable⇒UIP (_≡?_ : DecidableEquality A) where ≡-normalise : _≡_ {A = A} ⇒ _≡_ - ≡-normalise {x} {y} x≡y = recompute (x ≟ y) x≡y + ≡-normalise {x} {y} x≡y = recompute (x ≡? y) x≡y ≡-normalise-constant : (p q : x ≡ y) → ≡-normalise p ≡ ≡-normalise q - ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≟ y) + ≡-normalise-constant {x = x} {y = y} = recompute-constant (x ≡? y) ≡-irrelevant : UIP A ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant From 36754caca27b8f7b4593c4a3064082cad26290cd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 26 Feb 2026 10:41:44 +0000 Subject: [PATCH 12/20] add: better entry in `CHANGELOG`, plus tweak to `style-guide` --- CHANGELOG.md | 19 +++++++++++++++---- doc/style-guide.md | 2 +- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index eef65a4f16..77883ee67b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -21,6 +21,17 @@ Bug-fixes Non-backwards compatible changes -------------------------------- +* The notation for `Decidable` relations has been (partially) standardised: thus + - `_≡?_` (at `infix 4`) for `DecidableEquality` + - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence` + + Despite being non-backwards compatible, because a fieldname has changed, the + old notation `_≟_` (which was used for both of the above) has been retained, + but deprecated. This leads to a large amount of (trivial) deprecations, in + addition to the substantive one under `Relation.Binary.Structures`, and in + `Data.{Nat|Fin}.Properties` for the concrete datatypes. These deprecations + are summarised below, but are not each documented for each affected module. + Minor improvements ------------------ @@ -255,10 +266,10 @@ Additions to existing modules * In `Data.Fin.Properties`: ```agda ≡-irrelevant : Irrelevant {A = Fin n} _≡_ - ≡?-≡ : (eq : i ≡ j) → (i ≡? j) ≡ yes eq - ≡?-≡-refl : (i : Fin n) → (i ≡? i) ≡ yes refl - ≡?-≢ : (i≢j : i ≢ j) → (i ≡? j) ≡ no i≢j - inject-< : inject j < i + ≡?-≡ : (eq : i ≡ j) → (i ≡? j) ≡ yes eq + ≡?-≡-refl : (i : Fin n) → (i ≡? i) ≡ yes refl + ≡?-≢ : (i≢j : i ≢ j) → (i ≡? j) ≡ no i≢j + inject-< : inject j < i record Least⟨_⟩ (P : Pred (Fin n) p) : Set p where constructor least diff --git a/doc/style-guide.md b/doc/style-guide.md index 9ded0f896f..2714a94d4c 100644 --- a/doc/style-guide.md +++ b/doc/style-guide.md @@ -590,7 +590,7 @@ word within a compound word is capitalized except for the first word. where `R` is the underlying property being asserted to be `Decidable`, moreover typically sharing the same fixity and precedence as `R`: thus - `_≡?_` (at `infix 4`) for `DecidableEquality` - - `_≈?_` for the fieldname of the general `IsDecEquivalence` + - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence` * Any exceptions to these conventions should be flagged on the GitHub `agda-stdlib` issue tracker in the usual way. From 6a895bd86ee4c6b56b24ca15eea1f63beff6c971 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 13:17:49 +0000 Subject: [PATCH 13/20] tidy up `Relation.*` --- CHANGELOG.md | 5 +++ src/Data/Fin/Properties.agda | 1 - src/Relation/Binary/Consequences.agda | 4 +-- .../Binary/Construct/Add/Point/Equality.agda | 8 ++--- .../Closure/Reflexive/Properties.agda | 4 +-- .../Binary/Construct/NaturalOrder/Right.agda | 2 +- .../Lattice/Properties/JoinSemilattice.agda | 2 +- .../PropositionalEquality/Properties.agda | 4 +-- src/Relation/Nary.agda | 36 +++++++++++++------ src/Relation/Nullary/Decidable.agda | 2 +- 10 files changed, 43 insertions(+), 25 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 77883ee67b..5dd4295fe5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -125,6 +125,11 @@ Deprecated names ≢-≟-identity ↦ ≢-≡?-identity ``` +* In `Relation.Nary`: + ```agda + ≟-mapₙ ↦ ≡?-mapₙ + ``` + * In `Relation.Nullary.Decidable.Core`: ```agda ⊤-dec ↦ ⊤? diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index f3ea2a31b9..6f0d9dab42 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -1337,7 +1337,6 @@ _≟_ = _≡?_ Please use _≡?_ instead." #-} - ≟-≡-refl = ≡?-≡-refl {-# WARNING_ON_USAGE ≟-≡-refl "Warning: ≟-≡-refl was deprecated in v2.4. diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda index 43d91631ec..ee183c2ea5 100644 --- a/src/Relation/Binary/Consequences.agda +++ b/src/Relation/Binary/Consequences.agda @@ -79,9 +79,9 @@ module _ {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where total∧dec⇒dec : _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ → Total _≤_ → Decidable _≈_ → Decidable _≤_ - total∧dec⇒dec refl antisym total _≟_ x y with total x y + total∧dec⇒dec refl antisym total _≈?_ x y with total x y ... | inj₁ x≤y = yes x≤y - ... | inj₂ y≤x = map′ refl (flip antisym y≤x) (x ≟ y) + ... | inj₂ y≤x = map′ refl (flip antisym y≤x) (x ≈? y) module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃} {≤₂ : Rel B ℓ₄} where diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda index fdb3d9fee0..25609fffe6 100644 --- a/src/Relation/Binary/Construct/Add/Point/Equality.agda +++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda @@ -53,10 +53,10 @@ data _≈∙_ : Rel (Pointed A) (a ⊔ ℓ) where ≈∙-trans ≈-trans [ x≈y ] [ y≈z ] = [ ≈-trans x≈y y≈z ] ≈∙-dec : Decidable _≈_ → Decidable _≈∙_ -≈∙-dec _≟_ ∙ ∙ = yes ∙≈∙ -≈∙-dec _≟_ ∙ [ l ] = no (λ ()) -≈∙-dec _≟_ [ k ] ∙ = no (λ ()) -≈∙-dec _≟_ [ k ] [ l ] = Dec.map′ [_] [≈]-injective (k ≟ l) +≈∙-dec _≈?_ ∙ ∙ = yes ∙≈∙ +≈∙-dec _≈?_ ∙ [ l ] = no λ() +≈∙-dec _≈?_ [ k ] ∙ = no λ() +≈∙-dec _≈?_ [ k ] [ l ] = Dec.map′ [_] [≈]-injective (k ≈? l) ≈∙-irrelevant : Irrelevant _≈_ → Irrelevant _≈∙_ ≈∙-irrelevant ≈-irr ∙≈∙ ∙≈∙ = ≡.refl diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda index dce7099889..713ef58f3e 100644 --- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda +++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda @@ -135,7 +135,7 @@ module _ {_~_ : Rel A ℓ} where isDecPartialOrder O = record { isPartialOrder = isPartialOrder O.isStrictPartialOrder ; _≈?_ = O._≈?_ - ; _≤?_ = dec O._≟_ O._ Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r)) -≟-mapₙ n con con-inj = +≡?-mapₙ : ∀ n {ls} {as : Sets n ls} (con : Arrows n as R) → Injectiveₙ n con → + ∀ {l r} → Arrows n (Dec <$> Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r)) +≡?-mapₙ n con con-inj = curryₙ n λ a?s → let as? = Product-dec n a?s in Dec.map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as? @@ -205,5 +204,20 @@ toWitness : ∀ {n ls r} {as : Sets n ls} (R : as ⇉ Set r) (R? : Decidable R) ∀[ R ⇒ ⌊ R? ⌋ ] toWitness {zero} R R? with R? ... | true because _ = _ -... | no ¬r = ⊥-elim ∘′ ¬r +... | no ¬r = contradiction′ ¬r toWitness {suc n} R R? = toWitness (R _) (R? _) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +≟-mapₙ = ≡?-mapₙ +{-# WARNING_ON_USAGE ≟-mapₙ +"Warning: ≟-mapₙ was deprecated in v2.4. +Please use ≡?-mapₙ instead." +#-} diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda index e9e16a8c88..6caf11d5a1 100644 --- a/src/Relation/Nullary/Decidable.agda +++ b/src/Relation/Nullary/Decidable.agda @@ -47,7 +47,7 @@ module _ {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} (injection : Injection S T) open Injection injection via-injection : Decidable Eq₂._≈_ → Decidable Eq₁._≈_ - via-injection _≟_ x y = map′ injective cong (to x ≟ to y) + via-injection _≈?_ x y = map′ injective cong (to x ≈? to y) ------------------------------------------------------------------------ -- A lemma relating True and Dec From 93a74c6a4ff2318bdbd4b007356b60aa38f5732f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 13:22:40 +0000 Subject: [PATCH 14/20] tidy up `Reflection.*` --- src/Reflection/AST/AlphaEquality.agda | 31 ++++++++++++++++++++------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/src/Reflection/AST/AlphaEquality.agda b/src/Reflection/AST/AlphaEquality.agda index f6d1a7b1b5..dc9a7d3e5f 100644 --- a/src/Reflection/AST/AlphaEquality.agda +++ b/src/Reflection/AST/AlphaEquality.agda @@ -44,8 +44,8 @@ open AlphaEquality {{...}} public ------------------------------------------------------------------------ -- Utilities -≟⇒α : DecidableEquality A → AlphaEquality A -≟⇒α _≟_ = mkAlphaEquality (λ x y → ⌊ x ≟ y ⌋) +≡?⇒α : DecidableEquality A → AlphaEquality A +≡?⇒α _≡?_ = mkAlphaEquality (λ x y → ⌊ x ≡? y ⌋) ------------------------------------------------------------------------ -- Propositional cases @@ -55,22 +55,22 @@ open AlphaEquality {{...}} public instance α-Visibility : AlphaEquality Visibility - α-Visibility = ≟⇒α Visibility._≡?_ + α-Visibility = ≡?⇒α Visibility._≡?_ α-Modality : AlphaEquality Modality - α-Modality = ≟⇒α Modality._≡?_ + α-Modality = ≡?⇒α Modality._≡?_ α-ArgInfo : AlphaEquality ArgInfo - α-ArgInfo = ≟⇒α ArgInfo._≡?_ + α-ArgInfo = ≡?⇒α ArgInfo._≡?_ α-Literal : AlphaEquality Literal - α-Literal = ≟⇒α Literal._≡?_ + α-Literal = ≡?⇒α Literal._≡?_ α-Meta : AlphaEquality Meta - α-Meta = ≟⇒α Meta._≡?_ + α-Meta = ≡?⇒α Meta._≡?_ α-Name : AlphaEquality Name - α-Name = ≟⇒α Name._≡?_ + α-Name = ≡?⇒α Name._≡?_ ------------------------------------------------------------------------ -- Interesting cases @@ -344,3 +344,18 @@ instance α-ArgsPattern : AlphaEquality (Args Pattern) α-ArgsPattern = mkAlphaEquality _=α=-ArgsPattern_ + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +≟⇒α = ≡?⇒α +{-# WARNING_ON_USAGE ≟⇒α +"Warning: ≟⇒α was deprecated in v2.4. +Please use ≡?⇒α instead." +#-} From 1b273e95baaa0eddf07c8efdff58d4fa46d55fc6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 13:24:46 +0000 Subject: [PATCH 15/20] tidy up `Reflection.*` --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5dd4295fe5..5a7e1bb4c1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -119,6 +119,11 @@ Deprecated names truncate-irrelevant ↦ Relation.Binary.PropositionalEquality.Core.refl ``` +* In `Reflection.AST.AlphaEquality`: + ```agda + ≟⇒α ↦ ≡?⇒α + ``` + * In `Relation.Binary.PropositionalEquality`: ```agda ≡-≟-identity ↦ ≡-≡?-identity From d0946ba86115c90b90c74dd5758bbad277ef711b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 13:32:09 +0000 Subject: [PATCH 16/20] tidy up `Effect.Monad.Partiality` --- CHANGELOG.md | 5 +++++ src/Effect/Monad/Partiality.agda | 35 +++++++++++++++++++++++--------- 2 files changed, 30 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5a7e1bb4c1..e1c3c16a15 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -119,6 +119,11 @@ Deprecated names truncate-irrelevant ↦ Relation.Binary.PropositionalEquality.Core.refl ``` +* In `Effect.Monad.Partiality`: + ```agda + _≟-Kind_ ↦ _≡?-Kind_ + ``` + * In `Reflection.AST.AlphaEquality`: ```agda ≟⇒α ↦ ≡?⇒α diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda index d2bf58cac5..f1700c7b63 100644 --- a/src/Effect/Monad/Partiality.agda +++ b/src/Effect/Monad/Partiality.agda @@ -113,22 +113,22 @@ data Kind : Set where -- Kind equality is decidable. -infix 4 _≟-Kind_ +infix 4 _≡?-Kind_ -_≟-Kind_ : DecidableEquality Kind -_≟-Kind_ strong strong = yes ≡.refl -_≟-Kind_ strong (other k) = no λ() -_≟-Kind_ (other k) strong = no λ() -_≟-Kind_ (other geq) (other geq) = yes ≡.refl -_≟-Kind_ (other geq) (other weak) = no λ() -_≟-Kind_ (other weak) (other geq) = no λ() -_≟-Kind_ (other weak) (other weak) = yes ≡.refl +_≡?-Kind_ : DecidableEquality Kind +_≡?-Kind_ strong strong = yes ≡.refl +_≡?-Kind_ strong (other k) = no λ() +_≡?-Kind_ (other k) strong = no λ() +_≡?-Kind_ (other geq) (other geq) = yes ≡.refl +_≡?-Kind_ (other geq) (other weak) = no λ() +_≡?-Kind_ (other weak) (other geq) = no λ() +_≡?-Kind_ (other weak) (other weak) = yes ≡.refl -- A predicate which is satisfied only for equalities. Note that, for -- concrete inputs, this predicate evaluates to ⊤ or ⊥. Equality : Kind → Set -Equality k = False (k ≟-Kind other geq) +Equality k = False (k ≡?-Kind other geq) ------------------------------------------------------------------------ -- Equality/ordering @@ -933,3 +933,18 @@ idempotent {A = A} B x f = sound (idem x) laterˡ (refl (Setoid.refl B))) ⟩ (♭ x >>= λ y′ → ♭ x >>= λ y″ → f y′ y″) ≳⟨ idem (♭ x) ⟩≅ (♭ x >>= λ y′ → f y′ y′) ∎)) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +_≟-Kind_ = _≡?-Kind_ +{-# WARNING_ON_USAGE _≟-Kind_ +"Warning: _≟-Kind_ was deprecated in v2.4. +Please use _≡?-Kind_ instead." +#-} From 2f6403920785e62addbeec0e1c12caaab1a4feb3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 13:58:35 +0000 Subject: [PATCH 17/20] tidy up `Algebra` --- src/Algebra/Construct/LexProduct.agda | 8 +- src/Algebra/Construct/LexProduct/Base.agda | 4 +- src/Algebra/Construct/LexProduct/Inner.agda | 22 ++--- .../CancellativeCommutativeSemiring.agda | 4 +- src/Algebra/Solver/Monoid/Expression.agda | 4 +- src/Algebra/Solver/Monoid/ExpressionBAK.agda | 97 +++++++++++++++++++ src/Algebra/Solver/Monoid/Solver.agda | 2 +- 7 files changed, 119 insertions(+), 22 deletions(-) create mode 100644 src/Algebra/Solver/Monoid/ExpressionBAK.agda diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda index 3fbcf86c80..8a4cd45e47 100644 --- a/src/Algebra/Construct/LexProduct.agda +++ b/src/Algebra/Construct/LexProduct.agda @@ -21,7 +21,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning module Algebra.Construct.LexProduct {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄) - (_≟₁_ : Decidable (Magma._≈_ M)) + (_≈₁?_ : Decidable (Magma._≈_ M)) where open Magma M using (_∙_ ; ∙-cong) @@ -39,7 +39,7 @@ open Magma N using () ; refl to ≈₂-refl ) -import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex +import Algebra.Construct.LexProduct.Inner M N _≈₁?_ as InnerLex private infix 4 _≋_ @@ -53,7 +53,7 @@ private -- Definition ------------------------------------------------------------------------ -open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≟₁_ public +open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≈₁?_ public renaming (lex to _⊕_) ------------------------------------------------------------------------ @@ -103,7 +103,7 @@ identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈ identityʳ id₁ id₂ (x , a) = id₁ x , InnerLex.identityʳ id₁ id₂ sel : Selective _≈₁_ _∙_ → Selective _≈₂_ _◦_ → Selective _≋_ _⊕_ -sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | no ab≉a | no ab≉b = contradiction₂ (∙-sel a b) ab≉a ab≉b ... | yes ab≈a | no _ = inj₁ (ab≈a , ≈₂-refl) ... | no _ | yes ab≈b = inj₂ (ab≈b , ≈₂-refl) diff --git a/src/Algebra/Construct/LexProduct/Base.agda b/src/Algebra/Construct/LexProduct/Base.agda index 85686fd20c..585c8d730d 100644 --- a/src/Algebra/Construct/LexProduct/Base.agda +++ b/src/Algebra/Construct/LexProduct/Base.agda @@ -16,7 +16,7 @@ open import Relation.Nullary.Decidable.Core using (does; yes; no) module Algebra.Construct.LexProduct.Base {a b ℓ} {A : Set a} {B : Set b} (_∙_ : Op₂ A) (_◦_ : Op₂ B) - {_≈₁_ : Rel A ℓ} (_≟₁_ : Decidable _≈₁_) + {_≈₁_ : Rel A ℓ} (_≈₁?_ : Decidable _≈₁_) where ------------------------------------------------------------------------ @@ -27,7 +27,7 @@ module Algebra.Construct.LexProduct.Base -- operator that only calculates the second component of product. innerLex : A → A → B → B → B -innerLex a b x y with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b) +innerLex a b x y with does ((a ∙ b) ≈₁? a) | does ((a ∙ b) ≈₁? b) ... | true | false = x ... | false | true = y ... | _ | _ = x ◦ y diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda index beff9e9e3a..b6755e2528 100644 --- a/src/Algebra/Construct/LexProduct/Inner.agda +++ b/src/Algebra/Construct/LexProduct/Inner.agda @@ -21,7 +21,7 @@ import Algebra.Construct.LexProduct.Base as Base module Algebra.Construct.LexProduct.Inner {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄) - (_≟₁_ : Decidable (Magma._≈_ M)) + (_≈₁?_ : Decidable (Magma._≈_ M)) where open module M = Magma M @@ -48,7 +48,7 @@ private ------------------------------------------------------------------------ -- Base definition -open Base _∙_ _◦_ _≟₁_ public +open Base _∙_ _◦_ _≈₁?_ public using (innerLex) -- Save ourselves some typing in this file @@ -122,19 +122,19 @@ open SetoidReasoning N.setoid open NaturalOrder case₁ : a ∙ b ≈₁ a → a ∙ b ≉₁ b → lex a b x y ≈₂ x -case₁ {a} {b} ab≈a ab≉b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +case₁ {a} {b} ab≈a ab≉b with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | no ab≉a | _ = contradiction ab≈a ab≉a ... | yes _ | yes ab≈b = contradiction ab≈b ab≉b ... | yes _ | no _ = N.refl case₂ : a ∙ b ≉₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ y -case₂ {a} {b} ab≉a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +case₂ {a} {b} ab≉a ab≈b with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | yes ab≈a | _ = contradiction ab≈a ab≉a ... | no _ | no ab≉b = contradiction ab≈b ab≉b ... | no _ | yes _ = N.refl case₃ : a ∙ b ≈₁ a → a ∙ b ≈₁ b → lex a b x y ≈₂ (x ◦ y) -case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b +case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b ... | no ab≉a | _ = contradiction ab≈a ab≉a ... | yes _ | no ab≉b = contradiction ab≈b ab≉b ... | yes _ | yes _ = N.refl @@ -144,7 +144,7 @@ case₃ {a} {b} ab≈a ab≈b with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b cong : a ≈₁ b → c ≈₁ d → w ≈₂ x → y ≈₂ z → lex a c w y ≈₂ lex b d x z cong {a} {b} {c} {d} a≈b c≈d w≈x y≈z - with (a ∙ c) ≟₁ a | (a ∙ c) ≟₁ c | (b ∙ d) ≟₁ b | (b ∙ d) ≟₁ d + with (a ∙ c) ≈₁? a | (a ∙ c) ≈₁? c | (b ∙ d) ≈₁? b | (b ∙ d) ≈₁? d ... | yes _ | yes _ | yes _ | yes _ = ◦-cong w≈x y≈z ... | yes _ | yes _ | no _ | no _ = ◦-cong w≈x y≈z ... | no _ | no _ | yes _ | yes _ = ◦-cong w≈x y≈z @@ -172,7 +172,7 @@ assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ → Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ → ∀ a b c x y z → lex (a ∙ b) c (lex a b x y) z ≈₂ lex a (b ∙ c) x (lex b c y z) assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z - with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ c) ≟₁ b | (b ∙ c) ≟₁ c + with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b | (b ∙ c) ≈₁? b | (b ∙ c) ≈₁? c ... | _ | _ | no bc≉b | no bc≉c = contradiction₂ (∙-sel b c) bc≉b bc≉c ... | no ab≉a | no ab≉b | _ | _ = contradiction₂ (∙-sel a b) ab≉a ab≉b ... | yes ab≈a | no ab≉b | no bc≉b | yes bc≈c = cong₁₂ ab≈a (M.sym bc≈c) @@ -229,7 +229,7 @@ assoc ∙-assoc ∙-comm ∙-sel ◦-assoc a b c x y z comm : Commutative _≈₁_ _∙_ → Commutative _≈₂_ _◦_ → ∀ a b x y → lex a b x y ≈₂ lex b a y x comm ∙-comm ◦-comm a b x y - with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b | (b ∙ a) ≟₁ b | (b ∙ a) ≟₁ a + with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b | (b ∙ a) ≈₁? b | (b ∙ a) ≈₁? a ... | yes ab≈a | _ | _ | no ba≉a = contradiction (M.trans (∙-comm b a) ab≈a) ba≉a ... | no ab≉a | _ | _ | yes ba≈a = contradiction (M.trans (∙-comm a b) ba≈a) ab≉a ... | _ | yes ab≈b | no ba≉b | _ = contradiction (M.trans (∙-comm b a) ab≈b) ba≉b @@ -240,7 +240,7 @@ comm ∙-comm ◦-comm a b x y ... | no _ | no _ | no _ | no _ = ◦-comm x y idem : Idempotent _≈₂_ _◦_ → ∀ a b x → lex a b x x ≈₂ x -idem ◦-idem a b x with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b) +idem ◦-idem a b x with does ((a ∙ b) ≈₁? a) | does ((a ∙ b) ≈₁? b) ... | false | false = ◦-idem x ... | false | true = N.refl ... | true | false = N.refl @@ -248,14 +248,14 @@ idem ◦-idem a b x with does ((a ∙ b) ≟₁ a) | does ((a ∙ b) ≟₁ b) zeroʳ : ∀ {e f} → RightZero _≈₁_ e _∙_ → RightZero _≈₂_ f _◦_ → lex a e x f ≈₂ f -zeroʳ {a} {x} {e} {f} ze₁ ze₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e +zeroʳ {a} {x} {e} {f} ze₁ ze₂ with (a ∙ e) ≈₁? a | (a ∙ e) ≈₁? e ... | _ | no a∙e≉e = contradiction (ze₁ a) a∙e≉e ... | no _ | yes _ = N.refl ... | yes _ | yes _ = ze₂ x identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈₂_ f _◦_ → lex a e x f ≈₂ x -identityʳ {a} {x} {e} {f} id₁ id₂ with (a ∙ e) ≟₁ a | (a ∙ e) ≟₁ e +identityʳ {a} {x} {e} {f} id₁ id₂ with (a ∙ e) ≈₁? a | (a ∙ e) ≈₁? e ... | no a∙e≉a | _ = contradiction (id₁ a) a∙e≉a ... | yes _ | no _ = N.refl ... | yes _ | yes _ = id₂ x diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index 2062c33237..5d696058fd 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -26,7 +26,7 @@ open import Relation.Binary.Reasoning.Setoid setoid *-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0# -xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0# +xy≈0⇒x≈0∨y≈0 _≈?_ {x} {y} xy≈0 with x ≈? 0# | y ≈? 0# ... | yes x≈0 | _ = inj₁ x≈0 ... | no _ | yes y≈0 = inj₂ y≈0 ... | no x≉0 | no y≉0 = contradiction y≈0 y≉0 @@ -35,6 +35,6 @@ xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0# y≈0 = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0 x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0# -x≉0∧y≉0⇒xy≉0 _≟_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≟_ xy≈0 +x≉0∧y≉0⇒xy≉0 _≈?_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≈?_ xy≈0 ... | inj₁ x≈0 = x≉0 x≈0 ... | inj₂ y≈0 = y≉0 y≈0 diff --git a/src/Algebra/Solver/Monoid/Expression.agda b/src/Algebra/Solver/Monoid/Expression.agda index 7b71c9e9c2..3c28c07ffc 100644 --- a/src/Algebra/Solver/Monoid/Expression.agda +++ b/src/Algebra/Solver/Monoid/Expression.agda @@ -52,14 +52,14 @@ Env n = Vec Carrier n -- API for normal expressions record NormalAPI a : Set (suc a ⊔ c ⊔ ℓ) where - infix 5 _≟_ + infix 4 _≡?_ field -- The type of normal forms. Normal : ℕ → Set a -- We can decide if two normal forms are /syntactically/ equal. - _≟_ : DecidableEquality (Normal n) + _≡?_ : DecidableEquality (Normal n) -- A normaliser. normalise : Expr n → Normal n -- The semantics of a normal form. diff --git a/src/Algebra/Solver/Monoid/ExpressionBAK.agda b/src/Algebra/Solver/Monoid/ExpressionBAK.agda new file mode 100644 index 0000000000..74bbe4405e --- /dev/null +++ b/src/Algebra/Solver/Monoid/ExpressionBAK.agda @@ -0,0 +1,97 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- A solver for equations over monoids +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Algebra.Bundles.Raw using (RawMonoid) + +module Algebra.Solver.Monoid.ExpressionBAK {c ℓ} (M : RawMonoid c ℓ) where + +open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) +open import Data.Fin.Base using (Fin) +open import Data.Maybe.Base as Maybe using (Maybe) +open import Data.Nat.Base using (ℕ) +open import Data.Vec.Base using (Vec; lookup) +open import Level using (suc; _⊔_) +open import Relation.Binary.Consequences using (dec⇒weaklyDec) +open import Relation.Binary.Definitions using (DecidableEquality) +open import Relation.Binary.PropositionalEquality.Core using (_≡_) + +private + variable + n : ℕ + + module M = RawMonoid M + + +------------------------------------------------------------------------ +-- Monoid expressions + +-- There is one constructor for every operation, plus one for +-- variables; there may be at most n variables. + +infixr 5 _⊕_ + +data Expr (n : ℕ) : Set where + var : Fin n → Expr n + id : Expr n + _⊕_ : Expr n → Expr n → Expr n + +-- An environment contains one value for every variable. + +Env : ℕ → Set _ +Env n = Vec M.Carrier n + +-- The semantics of an expression is a function from an environment to +-- a value. + +⟦_⟧ : Expr n → Env n → M.Carrier +⟦ var x ⟧ ρ = lookup ρ x +⟦ id ⟧ ρ = M.ε +⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ M.∙ ⟦ e₂ ⟧ ρ + +------------------------------------------------------------------------ +-- API for normal expressions + +record Normal {a r} : Set (suc (a ⊔ r) ⊔ c ⊔ ℓ) where + infix 5 _≟_ + + field + + NF : ℕ → RawMonoid a r + + private + N : ℕ → Set a + N n = RawMonoid.Carrier (NF n) + + field + + ⟦var_⟧ : Fin n → N n + +-- We can decide if two normal forms are /syntactically/ equal. + + _≟_ : DecidableEquality (N n) + +-- The semantics of a normal form. + ⟦_⟧⇓ : N n → Env n → M.Carrier + + ⟦var_⟧⇓ : ∀ x ρ → ⟦ ⟦var x ⟧ ⟧⇓ ρ M.≈ lookup {n = n} ρ x + + ⟦_⟧⇓-homo : ∀ ρ → IsMonoidHomomorphism (NF n) M λ e → ⟦ e ⟧⇓ ρ + +-- A normaliser. + + module _ {n} where + + open RawMonoid (NF n) + + normalise : Expr n → N n + normalise (var x) = ⟦var x ⟧ + normalise id = ε + normalise (e₁ ⊕ e₂) = (normalise e₁) ∙ (normalise e₂) + + _semi≟_ : ∀ e₁ e₂ → Maybe (normalise e₁ ≡ normalise e₂) + e₁ semi≟ e₂ = dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) diff --git a/src/Algebra/Solver/Monoid/Solver.agda b/src/Algebra/Solver/Monoid/Solver.agda index a1281e9639..ab77687ed2 100644 --- a/src/Algebra/Solver/Monoid/Solver.agda +++ b/src/Algebra/Solver/Monoid/Solver.agda @@ -43,7 +43,7 @@ open R public -- for determining if two expressions have the same semantics. prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ) -prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂) +prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≡?_ (normalise e₁) (normalise e₂) where open import Relation.Binary.Reasoning.Setoid setoid lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ From b1762896f2003bec3c249f044402a3556ed55eac Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Feb 2026 15:31:37 +0000 Subject: [PATCH 18/20] refactor: tidy up the `Data.*` hierarchy --- src/Data/Fin/Induction.agda | 2 +- src/Data/List/Countdown.agda | 27 ++++++++-------- src/Data/List/Fresh/Membership/DecSetoid.agda | 4 +-- .../List/Membership/DecPropositional.agda | 4 +-- src/Data/List/Membership/DecSetoid.agda | 6 ++-- src/Data/List/Properties.agda | 10 +++--- .../Binary/Disjoint/DecPropositional.agda | 4 +-- .../Disjoint/Propositional/Properties.agda | 6 ++-- .../Binary/Disjoint/Setoid/Properties.agda | 8 ++--- .../Binary/Equality/DecPropositional.agda | 6 ++-- .../Relation/Binary/Equality/DecSetoid.agda | 2 +- .../List/Relation/Binary/Lex/NonStrict.agda | 8 ++--- src/Data/List/Relation/Binary/Lex/Strict.agda | 6 ++-- .../Propositional/Properties/WithK.agda | 10 +++--- .../Sublist/DecPropositional/Solver.agda | 4 +-- .../Binary/Sublist/DecSetoid/Solver.agda | 2 +- .../Binary/Subset/DecPropositional.agda | 4 +-- .../Unary/Enumerates/Setoid/Properties.agda | 4 +-- src/Data/List/Relation/Unary/Grouped.agda | 8 ++--- .../Unary/Unique/DecPropositional.agda | 4 +-- .../Unique/DecPropositional/Properties.agda | 8 ++--- .../Unary/Unique/DecSetoid/Properties.agda | 4 +-- src/Data/Maybe/Properties.agda | 8 ++--- src/Data/Parity/Properties.agda | 32 ++++++++++++++----- src/Data/Record.agda | 28 ++++++++-------- src/Data/Refinement.agda | 2 +- src/Data/Refinement/Properties.agda | 24 +++++++++++--- src/Data/Sign/Properties.agda | 32 ++++++++++++++----- src/Data/Sum/Relation/Binary/Pointwise.agda | 8 ++--- src/Data/Unit/Polymorphic.agda | 2 +- src/Data/Vec/Functional/Properties.agda | 6 ++-- src/Data/Vec/Membership/DecPropositional.agda | 4 +-- src/Data/Vec/Membership/DecSetoid.agda | 2 +- src/Data/Vec/Properties.agda | 6 ++-- .../Binary/Equality/DecPropositional.agda | 6 ++-- .../Relation/Binary/Equality/DecSetoid.agda | 2 +- .../Vec/Relation/Binary/Lex/NonStrict.agda | 22 ++++++------- 37 files changed, 187 insertions(+), 138 deletions(-) diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda index 6d0a9f9d72..81d9a47435 100644 --- a/src/Data/Fin/Induction.agda +++ b/src/Data/Fin/Induction.agda @@ -97,7 +97,7 @@ private >-weakInduction {n = n} P Pₙ Pᵢ₊₁⇒Pᵢ i = induct (>-wellFounded i) where induct : ∀ {i} → Acc _>_ i → P i - induct {i} (acc rec) with n ℕ.≟ toℕ i + induct {i} (acc rec) with n ℕ.≡? toℕ i ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ ... | no n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁) where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i))))) diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda index 746d91902c..4858be7337 100644 --- a/src/Data/List/Countdown.agda +++ b/src/Data/List/Countdown.agda @@ -36,8 +36,9 @@ open ≡.≡-Reasoning private open module D = DecSetoid D - hiding (refl) renaming (Carrier to Elem) - open import Data.List.Membership.Setoid D.setoid + using (_≈_; sym; trans; _≈?_; setoid) renaming (Carrier to Elem) + open import Data.List.Membership.DecSetoid D + using (_∈_; _∉_; _∈?_) ------------------------------------------------------------------------ -- Helper functions @@ -48,7 +49,7 @@ private first-occurrence : ∀ {xs} x → x ∈ xs → x ∈ xs first-occurrence x (here x≈y) = here x≈y - first-occurrence x (there {x = y} x∈xs) with x ≟ y + first-occurrence x (there {x = y} x∈xs) with x ≈? y ... | true because [x≈y] = here (invert [x≈y]) ... | false because _ = there $ first-occurrence x x∈xs @@ -67,12 +68,12 @@ private first-index x₁ x₁∈xs ≡ first-index x₂ x₂∈xs helper (here x₁≈x) (here x₂≈x) = refl helper (here x₁≈x) (there {x = x} x₂∈xs) - with x₂ ≟ x | dec-true (x₂ ≟ x) (trans (sym x₁≈x₂) x₁≈x) + with x₂ ≈? x | dec-true (x₂ ≈? x) (trans (sym x₁≈x₂) x₁≈x) ... | _ | refl = refl helper (there {x = x} x₁∈xs) (here x₂≈x) - with x₁ ≟ x | dec-true (x₁ ≟ x) (trans x₁≈x₂ x₂≈x) + with x₁ ≈? x | dec-true (x₁ ≈? x) (trans x₁≈x₂ x₂≈x) ... | _ | refl = refl - helper (there {x = x} x₁∈xs) (there x₂∈xs) with x₁ ≟ x | x₂ ≟ x + helper (there {x = x} x₁∈xs) (there x₂∈xs) with x₁ ≈? x | x₂ ≈? x ... | true because _ | true because _ = refl ... | false because _ | false because _ = cong suc $ helper x₁∈xs x₂∈xs ... | yes x₁≈x | no x₂≉x = contradiction (trans (sym x₁≈x₂) x₁≈x) x₂≉x @@ -88,13 +89,13 @@ private helper : ∀ {xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) → first-index x₁ x₁∈xs ≡ first-index x₂ x₂∈xs → x₁ ≈ x₂ helper (here x₁≈x) (here x₂≈x) _ = trans x₁≈x (sym x₂≈x) - helper (here x₁≈x) (there {x = x} x₂∈xs) _ with x₂ ≟ x + helper (here x₁≈x) (there {x = x} x₂∈xs) _ with x₂ ≈? x helper (here x₁≈x) (there {x = x} x₂∈xs) _ | yes x₂≈x = trans x₁≈x (sym x₂≈x) helper (here x₁≈x) (there {x = x} x₂∈xs) () | no x₂≉x - helper (there {x = x} x₁∈xs) (here x₂≈x) _ with x₁ ≟ x + helper (there {x = x} x₁∈xs) (here x₂≈x) _ with x₁ ≈? x helper (there {x = x} x₁∈xs) (here x₂≈x) _ | yes x₁≈x = trans x₁≈x (sym x₂≈x) helper (there {x = x} x₁∈xs) (here x₂≈x) () | no x₁≉x - helper (there {x = x} x₁∈xs) (there x₂∈xs) _ with x₁ ≟ x | x₂ ≟ x + helper (there {x = x} x₁∈xs) (there x₂∈xs) _ with x₁ ≈? x | x₂ ≈? x helper (there {x = x} x₁∈xs) (there x₂∈xs) _ | yes x₁≈x | yes x₂≈x = trans x₁≈x (sym x₂≈x) helper (there {x = x} x₁∈xs) (there x₂∈xs) () | yes x₁≈x | no x₂≉x helper (there {x = x} x₁∈xs) (there x₂∈xs) () | no x₁≉x | yes x₂≈x @@ -124,7 +125,7 @@ record _⊕_ (counted : List Elem) (n : ℕ) : Set where -- A countdown can be initialised by proving that Elem is finite. -empty : ∀ {n} → Injection D.setoid (≡.setoid (Fin n)) → [] ⊕ n +empty : ∀ {n} → Injection setoid (≡.setoid (Fin n)) → [] ⊕ n empty inj = record { kind = inj₂ ∘ to ; injective = λ {x} {y} {i} eq₁ eq₂ → injective (begin @@ -147,7 +148,7 @@ emptyFromList counted complete = empty record -- Finds out if an element has been counted yet. lookup : ∀ {counted n} → counted ⊕ n → ∀ x → Dec (x ∈ counted) -lookup {counted} _ x = Any.any? (_≟_ x) counted +lookup {counted} _ x = x ∈? counted -- When no element remains to be counted all elements have been -- counted. @@ -181,7 +182,7 @@ insert {counted} {n} counted⊕1+n x x∉counted = helper _ _ _ eq₁ eq₂ refl = injective eq₁ eq₂ kind′ : ∀ y → y ∈ x ∷ counted ⊎ Fin n - kind′ y with y ≟ x | kind x | kind y | helper x y + kind′ y with y ≈? x | kind x | kind y | helper x y kind′ y | yes y≈x | _ | _ | _ = inj₁ (here y≈x) kind′ y | _ | inj₁ x∈counted | _ | _ = contradiction x∈counted x∉counted kind′ y | _ | _ | inj₁ y∈counted | _ = inj₁ (there y∈counted) @@ -189,7 +190,7 @@ insert {counted} {n} counted⊕1+n x x∉counted = inj₂ (punchOut (y≉x ∘ sym ∘ hlp _ refl refl)) inj : ∀ {y z i} → kind′ y ≡ inj₂ i → kind′ z ≡ inj₂ i → y ≈ z - inj {y} {z} eq₁ eq₂ with y ≟ x | z ≟ x | kind x | kind y | kind z + inj {y} {z} eq₁ eq₂ with y ≈? x | z ≈? x | kind x | kind y | kind z | helper x y | helper x z | helper y z inj () _ | yes _ | _ | _ | _ | _ | _ | _ | _ inj _ () | _ | yes _ | _ | _ | _ | _ | _ | _ diff --git a/src/Data/List/Fresh/Membership/DecSetoid.agda b/src/Data/List/Fresh/Membership/DecSetoid.agda index 6a119d5d43..ddbf7ed495 100644 --- a/src/Data/List/Fresh/Membership/DecSetoid.agda +++ b/src/Data/List/Fresh/Membership/DecSetoid.agda @@ -17,7 +17,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary.Decidable using (¬?) -open DecSetoid DS using (setoid; _≟_) renaming (Carrier to A) +open DecSetoid DS using (setoid; _≈?_) renaming (Carrier to A) private variable @@ -34,7 +34,7 @@ open MembershipSetoid setoid public infix 4 _∈?_ _∉?_ _∈?_ : Decidable (_∈_ {R = R}) -x ∈? xs = any? (x ≟_) xs +x ∈? xs = any? (x ≈?_) xs _∉?_ : Decidable (_∉_ {R = R}) x ∉? xs = ¬? (x ∈? xs) diff --git a/src/Data/List/Membership/DecPropositional.agda b/src/Data/List/Membership/DecPropositional.agda index 3c81c0ff1e..559aa7aeda 100644 --- a/src/Data/List/Membership/DecPropositional.agda +++ b/src/Data/List/Membership/DecPropositional.agda @@ -9,7 +9,7 @@ open import Relation.Binary.Definitions using (DecidableEquality) module Data.List.Membership.DecPropositional - {a} {A : Set a} (_≟_ : DecidableEquality A) where + {a} {A : Set a} (_≡?_ : DecidableEquality A) where open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) @@ -17,5 +17,5 @@ open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) -- Re-export contents of propositional membership open import Data.List.Membership.Propositional {A = A} public -open import Data.List.Membership.DecSetoid (decSetoid _≟_) public +open import Data.List.Membership.DecSetoid (decSetoid _≡?_) public using (_∈?_; _∉?_) diff --git a/src/Data/List/Membership/DecSetoid.agda b/src/Data/List/Membership/DecSetoid.agda index 29fe88adb6..4b3d52cfde 100644 --- a/src/Data/List/Membership/DecSetoid.agda +++ b/src/Data/List/Membership/DecSetoid.agda @@ -14,12 +14,12 @@ open import Data.List.Relation.Unary.Any using (any?) open import Relation.Binary.Definitions using (Decidable) open import Relation.Nullary.Decidable using (¬?) -open DecSetoid DS +open DecSetoid DS using (_≈?_; setoid) ------------------------------------------------------------------------ -- Re-export contents of propositional membership -open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public +open import Data.List.Membership.Setoid setoid public ------------------------------------------------------------------------ -- Other operations @@ -27,7 +27,7 @@ open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public infix 4 _∈?_ _∉?_ _∈?_ : Decidable _∈_ -x ∈? xs = any? (x ≟_) xs +x ∈? xs = any? (x ≈?_) xs _∉?_ : Decidable _∉_ x ∉? xs = ¬? (x ∈? xs) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 370676e601..0674b2fff1 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -76,13 +76,13 @@ private ∷-injectiveʳ refl = refl ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y List.∷ ys) -∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys) +∷-dec x≡?y xs≡?ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≡?y ×-dec xs≡?ys) ≡-dec : DecidableEquality A → DecidableEquality (List A) -≡-dec _≟_ [] [] = yes refl -≡-dec _≟_ (x ∷ xs) [] = no λ() -≡-dec _≟_ [] (y ∷ ys) = no λ() -≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys) +≡-dec _≈?_ [] [] = yes refl +≡-dec _≈?_ (x ∷ xs) [] = no λ() +≡-dec _≈?_ [] (y ∷ ys) = no λ() +≡-dec _≈?_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≈? y) (≡-dec _≈?_ xs ys) ------------------------------------------------------------------------ -- map diff --git a/src/Data/List/Relation/Binary/Disjoint/DecPropositional.agda b/src/Data/List/Relation/Binary/Disjoint/DecPropositional.agda index 82d39c261f..e4667a4905 100644 --- a/src/Data/List/Relation/Binary/Disjoint/DecPropositional.agda +++ b/src/Data/List/Relation/Binary/Disjoint/DecPropositional.agda @@ -9,7 +9,7 @@ open import Relation.Binary.Definitions using (DecidableEquality) module Data.List.Relation.Binary.Disjoint.DecPropositional - {a} {A : Set a} (_≟_ : DecidableEquality A) + {a} {A : Set a} (_≡?_ : DecidableEquality A) where ------------------------------------------------------------------------ @@ -17,5 +17,5 @@ module Data.List.Relation.Binary.Disjoint.DecPropositional open import Data.List.Relation.Binary.Disjoint.Propositional {A = A} public open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) -open import Data.List.Relation.Binary.Disjoint.DecSetoid (decSetoid _≟_) public +open import Data.List.Relation.Binary.Disjoint.DecSetoid (decSetoid _≡?_) public using (disjoint?) diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda index 23021265d2..33af44c765 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Propositional/Properties.agda @@ -61,6 +61,6 @@ module _ {a} {A : Set a} where concat⁺ʳ = S.concat⁺ʳ (setoid _) -- deduplicate - module _ (_≟_ : DecidableEquality A) where - deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys) - deduplicate⁺ = S.deduplicate⁺ Sᴬ _≟_ + module _ (_≡?_ : DecidableEquality A) where + deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≡?_ xs) (deduplicate _≡?_ ys) + deduplicate⁺ = S.deduplicate⁺ Sᴬ _≡?_ diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda index 3416fc31e8..9d439af381 100644 --- a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda @@ -22,7 +22,7 @@ open import Data.Sum.Base using (inj₁; inj₂) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Definitions using (Symmetric; DecidableEquality) open import Relation.Binary.PropositionalEquality.Core using (_≡_) -open import Relation.Nullary.Negation using (¬_) +open import Relation.Nullary.Negation.Core using (¬_) module _ {c ℓ} (S : Setoid c ℓ) where @@ -56,9 +56,9 @@ module _ {c ℓ} (S : Setoid c ℓ) where ... | inj₂ v∈xss = concat⁺ʳ vs#xss (v∈vs , v∈xss) -- deduplicate - module _ (_≟_ : DecidableEquality A) where + module _ (_≡?_ : DecidableEquality A) where deduplicate⁺ : ∀ {xs ys} → Disjoint S xs ys → - Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys) - deduplicate⁺ = let ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≟_ in + Disjoint S (deduplicate _≡?_ xs) (deduplicate _≡?_ ys) + deduplicate⁺ = let ∈-dedup⁻ = Mem.∈-deduplicate⁻ S _≡?_ in _∘ Product.map (∈-dedup⁻ _) (∈-dedup⁻ _) diff --git a/src/Data/List/Relation/Binary/Equality/DecPropositional.agda b/src/Data/List/Relation/Binary/Equality/DecPropositional.agda index 8f6b20ec99..ad15a890f1 100644 --- a/src/Data/List/Relation/Binary/Equality/DecPropositional.agda +++ b/src/Data/List/Relation/Binary/Equality/DecPropositional.agda @@ -13,7 +13,7 @@ open import Relation.Binary.Definitions using (DecidableEquality) module Data.List.Relation.Binary.Equality.DecPropositional - {a} {A : Set a} (_≟_ : DecidableEquality A) where + {a} {A : Set a} (_≈?_ : DecidableEquality A) where open import Data.List.Base using (List) open import Data.List.Properties using (≡-dec) @@ -26,7 +26,7 @@ open import Relation.Binary.PropositionalEquality.Properties using (decSetoid) -- equality open PropositionalEq public -open DecSetoidEq (decSetoid _≟_) public +open DecSetoidEq (decSetoid _≈?_) public using (_≋?_; ≋-isDecEquivalence; ≋-decSetoid) ------------------------------------------------------------------------ @@ -35,4 +35,4 @@ open DecSetoidEq (decSetoid _≟_) public infix 4 _≡?_ _≡?_ : DecidableEquality (List A) -_≡?_ = ≡-dec _≟_ +_≡?_ = ≡-dec _≈?_ diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda index d0c4ab6923..2efa6dc71e 100644 --- a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda +++ b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda @@ -23,7 +23,7 @@ open DecSetoid DS using (setoid) open DecSetoid ≋-decSetoid public using () - renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_) + renaming (isDecEquivalence to ≋-isDecEquivalence; _≈?_ to _≋?_) ------------------------------------------------------------------------ -- Make all definitions from setoid equality available diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda index 893620d3ff..c500292644 100644 --- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda +++ b/src/Data/List/Relation/Binary/Lex/NonStrict.agda @@ -83,12 +83,12 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where <-compare : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ → Total _≼_ → Trichotomous _≋_ _<_ - <-compare sym _≟_ antisym tot = - Strict.<-compare sym (Conv.<-trichotomous _ _ sym _≟_ antisym tot) + <-compare sym _≈?_ antisym tot = + Strict.<-compare sym (Conv.<-trichotomous _ _ sym _≈?_ antisym tot) <-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _<_ - <-decidable _≟_ _≼?_ = - Core.decidable (no id) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_) + <-decidable _≈?_ _≼?_ = + Core.decidable (no id) _≈?_ (Conv.<-decidable _ _ _≈?_ _≼?_) <-isStrictPartialOrder : IsPartialOrder _≈_ _≼_ → IsStrictPartialOrder _≋_ _<_ diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda index f274241522..301144d23c 100644 --- a/src/Data/List/Relation/Binary/Lex/Strict.agda +++ b/src/Data/List/Relation/Binary/Lex/Strict.agda @@ -204,7 +204,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where ≤-isDecPartialOrder sto = record { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder ; _≈?_ = Pointwise.decidable _≈?_ - ; _≤?_ = ≤-decidable _≟_ _ Date: Fri, 27 Feb 2026 16:00:37 +0000 Subject: [PATCH 19/20] fix: `README.Design.Decidability` --- doc/README/Design/Decidability.agda | 84 ++++++++++++++--------------- 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/doc/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda index 63ab9f2021..a32fb8782f 100644 --- a/doc/README/Design/Decidability.agda +++ b/doc/README/Design/Decidability.agda @@ -24,21 +24,21 @@ open import Relation.Nary open import Relation.Nullary.Reflects -infix 4 _≟₀_ _≟₁_ _≟₂_ +infix 4 _≡?₀_ _≡?₁_ _≡?₂_ -- A proof of `Reflects P b` shows that a proposition `P` has the truth value of -- the boolean `b`. A proof of `Reflects P true` amounts to a proof of `P`, and -- a proof of `Reflects P false` amounts to a refutation of `P`. ex₀ : (n : ℕ) → Reflects (n ≡ n) true -ex₀ n = ofʸ refl +ex₀ n = of refl ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false -ex₁ n = ofⁿ λ () +ex₁ n = of λ() ex₂ : (b : Bool) → Reflects (T b) b -ex₂ false = ofⁿ id -ex₂ true = ofʸ tt +ex₂ false = of id +ex₂ true = of tt ------------------------------------------------------------------------ -- Dec @@ -64,71 +64,71 @@ ex₄ n = no λ () -- only the `yes` and `no` patterns. The following procedure decides whether two -- given natural numbers are equal. -_≟₀_ : (m n : ℕ) → Dec (m ≡ n) -zero ≟₀ zero = yes refl -zero ≟₀ suc n = no λ () -suc m ≟₀ zero = no λ () -suc m ≟₀ suc n with m ≟₀ n +_≡?₀_ : (m n : ℕ) → Dec (m ≡ n) +zero ≡?₀ zero = yes refl +zero ≡?₀ suc n = no λ() +suc m ≡?₀ zero = no λ() +suc m ≡?₀ suc n with m ≡?₀ n ... | yes p = yes (cong suc p) ... | no ¬p = no (¬p ∘ suc-injective) --- In this case, we can see that `does (suc m ≟ suc n)` should be equal to --- `does (m ≟ n)`, because a `yes` from `m ≟ n` gives rise to a `yes` from the +-- In this case, we can see that `does (suc m ≡? suc n)` should be equal to +-- `does (m ≡? n)`, because a `yes` from `m ≡? n` gives rise to a `yes` from the -- result, and similarly for `no`. However, in the above definition, this -- equality does not hold definitionally, because we always do a case split -- before returning a result. To avoid this, we can return the `does` part -- separately, before any pattern matching. -_≟₁_ : (m n : ℕ) → Dec (m ≡ n) -zero ≟₁ zero = yes refl -zero ≟₁ suc n = no λ () -suc m ≟₁ zero = no λ () -does (suc m ≟₁ suc n) = does (m ≟₁ n) -proof (suc m ≟₁ suc n) with m ≟₁ n -... | yes p = ofʸ (cong suc p) -... | no ¬p = ofⁿ (¬p ∘ suc-injective) +_≡?₁_ : (m n : ℕ) → Dec (m ≡ n) +zero ≡?₁ zero = yes refl +zero ≡?₁ suc n = no λ() +suc m ≡?₁ zero = no λ() +does (suc m ≡?₁ suc n) = does (m ≡?₁ n) +proof (suc m ≡?₁ suc n) with m ≡?₁ n +... | yes p = of (cong suc p) +... | no ¬p = of (¬p ∘ suc-injective) -- We now get definitional equalities such as the following. -_ : (m n : ℕ) → does (5 + m ≟₁ 3 + n) ≡ does (2 + m ≟₁ n) +_ : (m n : ℕ) → does (5 + m ≡?₁ 3 + n) ≡ does (2 + m ≡?₁ n) _ = λ m n → refl -- Even better, from a maintainability point of view, is to use `map` or `map′`, -- both of which capture the pattern of the `does` field remaining the same, but -- the `proof` field being updated. -_≟₂_ : (m n : ℕ) → Dec (m ≡ n) -zero ≟₂ zero = yes refl -zero ≟₂ suc n = no λ () -suc m ≟₂ zero = no λ () -suc m ≟₂ suc n = map′ (cong suc) suc-injective (m ≟₂ n) +_≡?₂_ : (m n : ℕ) → Dec (m ≡ n) +zero ≡?₂ zero = yes refl +zero ≡?₂ suc n = no λ() +suc m ≡?₂ zero = no λ() +suc m ≡?₂ suc n = map′ (cong suc) suc-injective (m ≡?₂ n) -_ : (m n : ℕ) → does (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n) +_ : (m n : ℕ) → does (5 + m ≡?₂ 3 + n) ≡ does (2 + m ≡?₂ n) _ = λ m n → refl -- `map′` can be used in conjunction with combinators such as `_⊎?_` and -- `_×?_` to build complex (simply typed) decision procedures. -module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where +module ListDecEq₀ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where - _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) - [] ≟ᴸᴬ [] = yes refl - [] ≟ᴸᴬ (y ∷ ys) = no λ () - (x ∷ xs) ≟ᴸᴬ [] = no λ () - (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = - map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×? xs ≟ᴸᴬ ys) + _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) + [] ≡?ᴸᴬ [] = yes refl + [] ≡?ᴸᴬ (y ∷ ys) = no λ() + (x ∷ xs) ≡?ᴸᴬ [] = no λ() + (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) = + map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≡?ᴬ y ×? xs ≡?ᴸᴬ ys) -- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and* -- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`. -- In the case of ≡-equality tests, the pattern --- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×? ... ×? xₙ₋₁ ≟ yₙ₋₁)` --- is captured by `≟-mapₙ n c c-injective (x₀ ≟ y₀) ... (xₙ₋₁ ≟ yₙ₋₁)`. +-- `map′ (congₙ c) c-injective (x₀ ≡? y₀ ×? ... ×? xₙ₋₁ ≡? yₙ₋₁)` +-- is captured by `≡?-mapₙ n c c-injective (x₀ ≡? y₀) ... (xₙ₋₁ ≡? yₙ₋₁)`. -module ListDecEq₁ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where +module ListDecEq₁ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where - _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) - [] ≟ᴸᴬ [] = yes refl - [] ≟ᴸᴬ (y ∷ ys) = no λ () - (x ∷ xs) ≟ᴸᴬ [] = no λ () - (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = ≟-mapₙ 2 _∷_ ∷-injective (x ≟ᴬ y) (xs ≟ᴸᴬ ys) + _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys) + [] ≡?ᴸᴬ [] = yes refl + [] ≡?ᴸᴬ (y ∷ ys) = no λ() + (x ∷ xs) ≡?ᴸᴬ [] = no λ() + (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) = ≡?-mapₙ 2 _∷_ ∷-injective (x ≡?ᴬ y) (xs ≡?ᴸᴬ ys) From 00c55e19374f1bcbd9ed3beed71936564d714931 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 28 Feb 2026 03:14:05 +0000 Subject: [PATCH 20/20] fix: remove module added in error --- src/Algebra/Solver/Monoid/ExpressionBAK.agda | 97 -------------------- 1 file changed, 97 deletions(-) delete mode 100644 src/Algebra/Solver/Monoid/ExpressionBAK.agda diff --git a/src/Algebra/Solver/Monoid/ExpressionBAK.agda b/src/Algebra/Solver/Monoid/ExpressionBAK.agda deleted file mode 100644 index 74bbe4405e..0000000000 --- a/src/Algebra/Solver/Monoid/ExpressionBAK.agda +++ /dev/null @@ -1,97 +0,0 @@ ------------------------------------------------------------------------- --- The Agda standard library --- --- A solver for equations over monoids ------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Algebra.Bundles.Raw using (RawMonoid) - -module Algebra.Solver.Monoid.ExpressionBAK {c ℓ} (M : RawMonoid c ℓ) where - -open import Algebra.Morphism.Structures using (IsMonoidHomomorphism) -open import Data.Fin.Base using (Fin) -open import Data.Maybe.Base as Maybe using (Maybe) -open import Data.Nat.Base using (ℕ) -open import Data.Vec.Base using (Vec; lookup) -open import Level using (suc; _⊔_) -open import Relation.Binary.Consequences using (dec⇒weaklyDec) -open import Relation.Binary.Definitions using (DecidableEquality) -open import Relation.Binary.PropositionalEquality.Core using (_≡_) - -private - variable - n : ℕ - - module M = RawMonoid M - - ------------------------------------------------------------------------- --- Monoid expressions - --- There is one constructor for every operation, plus one for --- variables; there may be at most n variables. - -infixr 5 _⊕_ - -data Expr (n : ℕ) : Set where - var : Fin n → Expr n - id : Expr n - _⊕_ : Expr n → Expr n → Expr n - --- An environment contains one value for every variable. - -Env : ℕ → Set _ -Env n = Vec M.Carrier n - --- The semantics of an expression is a function from an environment to --- a value. - -⟦_⟧ : Expr n → Env n → M.Carrier -⟦ var x ⟧ ρ = lookup ρ x -⟦ id ⟧ ρ = M.ε -⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ M.∙ ⟦ e₂ ⟧ ρ - ------------------------------------------------------------------------- --- API for normal expressions - -record Normal {a r} : Set (suc (a ⊔ r) ⊔ c ⊔ ℓ) where - infix 5 _≟_ - - field - - NF : ℕ → RawMonoid a r - - private - N : ℕ → Set a - N n = RawMonoid.Carrier (NF n) - - field - - ⟦var_⟧ : Fin n → N n - --- We can decide if two normal forms are /syntactically/ equal. - - _≟_ : DecidableEquality (N n) - --- The semantics of a normal form. - ⟦_⟧⇓ : N n → Env n → M.Carrier - - ⟦var_⟧⇓ : ∀ x ρ → ⟦ ⟦var x ⟧ ⟧⇓ ρ M.≈ lookup {n = n} ρ x - - ⟦_⟧⇓-homo : ∀ ρ → IsMonoidHomomorphism (NF n) M λ e → ⟦ e ⟧⇓ ρ - --- A normaliser. - - module _ {n} where - - open RawMonoid (NF n) - - normalise : Expr n → N n - normalise (var x) = ⟦var x ⟧ - normalise id = ε - normalise (e₁ ⊕ e₂) = (normalise e₁) ∙ (normalise e₂) - - _semi≟_ : ∀ e₁ e₂ → Maybe (normalise e₁ ≡ normalise e₂) - e₁ semi≟ e₂ = dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)