------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a single relation
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary

module Relation.Binary.Reasoning.Base.Single
  {a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
  (refl : Reflexive _∼_) (trans : Transitive _∼_)
  where

------------------------------------------------------------------------
-- Reasoning combinators

-- Re-export combinators from partial reasoning

open import Relation.Binary.Reasoning.Base.Partial _∼_ trans public
  hiding (_∎⟨_⟩)

-- Redefine the terminating combinator now that we have reflexivity

infix   _∎

_∎ : ∀ x → x IsRelatedTo x
x ∎ = relTo refl