diff options
author | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:18 -0700 |
---|---|---|
committer | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:18 -0700 |
commit | a19b25a865b2000bbd3acd909f5951a5407c1eec (patch) | |
tree | e283a809447d00f63289a918e6fd0f73ee0b8ece /src/Relation/Binary/EqReasoning.agda | |
parent | 0b3946998d82e1be6c50e2872e7474db69b5a0dc (diff) |
New upstream version 0.17
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 _≡⟨⟩_ + ) + |