diff options
| author | Sean Whitton <spwhitton@spwhitton.name> | 2016-06-10 17:28:53 +0900 |
|---|---|---|
| committer | Sean Whitton <spwhitton@spwhitton.name> | 2016-06-10 17:28:53 +0900 |
| commit | 4b8a7e1e9640da64fd17a74ebc176909a3aea944 (patch) | |
| tree | 9b85ed495daeb8968d8cd9f7abd45a8244e341b1 /src/Relation/Binary/EqReasoning.agda | |
| parent | 22d7b46b012db080c7e94b064eef55fc25b31eac (diff) | |
Imported Upstream version 0.12
Diffstat (limited to 'src/Relation/Binary/EqReasoning.agda')
| -rw-r--r-- | src/Relation/Binary/EqReasoning.agda | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/Relation/Binary/EqReasoning.agda b/src/Relation/Binary/EqReasoning.agda index cee1043..394cb50 100644 --- a/src/Relation/Binary/EqReasoning.agda +++ b/src/Relation/Binary/EqReasoning.agda @@ -19,10 +19,8 @@ -- 0 -- ∎ --- Note that some modules contain generalised versions of specific --- instantiations of this module. For instance, the module ≡-Reasoning --- in Relation.Binary.PropositionalEquality is recommended for --- equational reasoning when the underlying equality is +-- Module ≡-Reasoning in Relation.Binary.PropositionalEquality +-- is recommended for equational reasoning when the underlying equality is -- Relation.Binary.PropositionalEquality._≡_. open import Relation.Binary |