diff options
| author | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:46 -0700 |
|---|---|---|
| committer | Sean Whitton <spwhitton@spwhitton.name> | 2018-11-23 17:29:46 -0700 |
| commit | 5a91775bd7c909bbaf3b3c8ee964136961a5146d (patch) | |
| tree | cea89f085c1382f1567ff71a30b6f953708dc6a9 /src/Relation/Binary/EqReasoning.agda | |
| parent | 5d2b156377dce5bdca65b14639306eaed3ac3a92 (diff) | |
| parent | a19b25a865b2000bbd3acd909f5951a5407c1eec (diff) | |
Merge tag 'upstream/0.17'
Upstream version 0.17
# gpg: Signature made Fri 23 Nov 2018 05:29:18 PM MST
# gpg: using RSA key 9B917007AE030E36E4FC248B695B7AE4BF066240
# gpg: issuer "spwhitton@spwhitton.name"
# gpg: Good signature from "Sean Whitton <spwhitton@spwhitton.name>" [ultimate]
# Primary key fingerprint: 8DC2 487E 51AB DD90 B5C4 753F 0F56 D055 3B6D 411B
# Subkey fingerprint: 9B91 7007 AE03 0E36 E4FC 248B 695B 7AE4 BF06 6240
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 _≡⟨⟩_ + ) + |