Imported Upstream version 0.3

1 files changed, 37 insertions, 0 deletions

diff --git a/src/Relation/Binary/EqReasoning.agda b/src/Relation/Binary/EqReasoning.agda
new file mode 100644
index 0000000..44321d1
--- /dev/null
+++ b/src/Relation/Binary/EqReasoning.agda
@@ -0,0 +1,37 @@
+------------------------------------------------------------------------
+-- Convenient syntax for equational reasoning
+------------------------------------------------------------------------
+
+{-# OPTIONS --universe-polymorphism #-}
+
+-- Example use:
+
+-- n*0≡0 : ∀ n → n * 0 ≡ 0
+-- n*0≡0 zero    = refl
+-- n*0≡0 (suc n) =
+--   begin
+--     suc n * 0
+--   ≈⟨ refl ⟩
+--     n * 0 + 0
+--   ≈⟨ ... ⟩
+--     n * 0
+--   ≈⟨ n*0≡0 n ⟩
+--     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
+-- Relation.Binary.PropositionalEquality._≡_.
+
+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 _≡⟨_⟩_
+                )