From da2dd6a13df9e6b3c147bca2c3a79a9b7930bc74 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 2 Oct 2024 12:27:24 +0100 Subject: [PATCH] fixed knock-on ambiguity bugs --- CHANGELOG.md | 1 + src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda | 2 +- src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 14346f3c0a..fbbb337894 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -114,6 +114,7 @@ New modules ```agda Relation.Binary.Bundles.Raw ``` + plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`. Additions to existing modules ----------------------------- diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda index 49da62b10b..8b3ba8b55e 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda @@ -29,7 +29,7 @@ open import Relation.Unary using (Pred; _∩_) open import Data.Tree.AVL.Indexed sto as AVL open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any -open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (_≉_; sym; trans) +open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans) open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective) diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda index fefb27764f..2368c44bcd 100644 --- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda +++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda @@ -30,7 +30,7 @@ open import Relation.Nullary using (Reflects; ¬_; yes; no) open import Relation.Nullary.Negation using (contradiction) open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans) -open Eq using (_≉_; refl; sym; trans) +open Eq using (refl; sym; trans) open import Data.Tree.AVL strictTotalOrder using (tree) open import Data.Tree.AVL.Indexed strictTotalOrder using (key) import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny