------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for reasoning with a setoid
------------------------------------------------------------------------
-- 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 ∎
-- Module `≡-Reasoning` in `Relation.Binary.PropositionalEquality`
-- is recommended for equational reasoning when the underlying equality
-- is `_≡_`.
{-#
OPTIONS
--cubical-compatible
--safe
#-}
open
import
Relation.Binary.Bundles
using
(
Setoid
)
open
import
Relation.Binary.Reasoning.Syntax
using
(
module
≈-syntax
)
module
Relation.Binary.Reasoning.Setoid
{
s₁
s₂
}
(
S
:
Setoid
s₁
s₂
)
where
open
Setoid
S
import
Relation.Binary.Reasoning.Base.Single
_≈_
refl
trans
as
SingleRelReasoning
------------------------------------------------------------------------
-- Reasoning combinators
-- Export the combinators for single relation reasoning, hiding the
-- single misnamed combinator.
open
SingleRelReasoning
public
hiding
(
step-∼
)
renaming
(
∼-go
to
≈-go
)
-- Re-export the equality-based combinators instead
open
≈-syntax
_IsRelatedTo_
_IsRelatedTo_
≈-go
sym
public