1
------------------------------------------------------------------------
2
-- Convenient syntax for "equational reasoning" using a strict partial
4
------------------------------------------------------------------------
6
{-# OPTIONS --universe-polymorphism #-}
8
open import Relation.Binary
10
module Relation.Binary.StrictPartialOrderReasoning
11
{p₁ p₂ p₃} (S : StrictPartialOrder p₁ p₂ p₃) where
13
import Relation.Binary.PreorderReasoning as PreR
14
import Relation.Binary.Props.StrictPartialOrder as SPO
15
open PreR (SPO.preorder S) public renaming (_∼⟨_⟩_ to _<⟨_⟩_)