summaryrefslogtreecommitdiff
path: root/src/Relation/Binary/EqReasoning.agda
diff options
context:
space:
mode:
Diffstat (limited to 'src/Relation/Binary/EqReasoning.agda')
-rw-r--r--src/Relation/Binary/EqReasoning.agda13
1 files changed, 7 insertions, 6 deletions
diff --git a/src/Relation/Binary/EqReasoning.agda b/src/Relation/Binary/EqReasoning.agda
index 394cb50..c498059 100644
--- a/src/Relation/Binary/EqReasoning.agda
+++ b/src/Relation/Binary/EqReasoning.agda
@@ -28,9 +28,10 @@ open import Relation.Binary
module Relation.Binary.EqReasoning {s₁ s₂} (S : Setoid s₁ s₂) where
open Setoid S
-import Relation.Binary.PreorderReasoning as PreR
-open PreR preorder public
- renaming ( _∼⟨_⟩_ to _≈⟨_⟩_
- ; _≈⟨_⟩_ to _≡⟨_⟩_
- ; _≈⟨⟩_ to _≡⟨⟩_
- )
+open import Relation.Binary.PreorderReasoning preorder public
+ hiding (_≈⟨_⟩_)
+ renaming
+ ( _∼⟨_⟩_ to _≈⟨_⟩_
+ ; _≈⟨⟩_ to _≡⟨⟩_
+ )
+