------------------------------------------------------------------------
-- 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