diff options
Diffstat (limited to 'src/Relation/Binary/EqReasoning.agda')
-rw-r--r-- | src/Relation/Binary/EqReasoning.agda | 13 |
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 _≡⟨⟩_ + ) + |