/usr/share/agda-stdlib/Relation/Binary/StrictPartialOrderReasoning.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a strict partial
-- order
------------------------------------------------------------------------
open import Relation.Binary
module Relation.Binary.StrictPartialOrderReasoning
{p₁ p₂ p₃} (S : StrictPartialOrder p₁ p₂ p₃) where
import Relation.Binary.PreorderReasoning as PreR
import Relation.Binary.Props.StrictPartialOrder as SPO
open PreR (SPO.preorder S) public renaming (_∼⟨_⟩_ to _<⟨_⟩_)
|