/usr/share/doc/agda-stdlib-doc/html/Relation.Binary.PartialOrderReasoning.html is in agda-stdlib-doc 0.14-1.
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 16 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Binary.PartialOrderReasoning</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Convenient syntax for "equational reasoning" using a partial order</a>
<a id="176" class="Comment">------------------------------------------------------------------------</a>
<a id="250" class="Keyword">open</a> <a id="255" class="Keyword">import</a> <a id="262" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="279" class="Keyword">module</a> <a id="286" href="Relation.Binary.PartialOrderReasoning.html" class="Module">Relation.Binary.PartialOrderReasoning</a>
<a id="333" class="Symbol">{</a><a id="334" href="Relation.Binary.PartialOrderReasoning.html#334" class="Bound">p₁</a> <a id="337" href="Relation.Binary.PartialOrderReasoning.html#337" class="Bound">p₂</a> <a id="340" href="Relation.Binary.PartialOrderReasoning.html#340" class="Bound">p₃</a><a id="342" class="Symbol">}</a> <a id="344" class="Symbol">(</a><a id="345" href="Relation.Binary.PartialOrderReasoning.html#345" class="Bound">P</a> <a id="347" class="Symbol">:</a> <a id="349" href="Relation.Binary.html#Poset" class="Record">Poset</a> <a id="355" href="Relation.Binary.PartialOrderReasoning.html#334" class="Bound">p₁</a> <a id="358" href="Relation.Binary.PartialOrderReasoning.html#337" class="Bound">p₂</a> <a id="361" href="Relation.Binary.PartialOrderReasoning.html#340" class="Bound">p₃</a><a id="363" class="Symbol">)</a> <a id="365" class="Keyword">where</a>
<a id="372" class="Keyword">open</a> <a id="377" href="Relation.Binary.html#Poset" class="Module">Poset</a> <a id="383" href="Relation.Binary.PartialOrderReasoning.html#345" class="Bound">P</a>
<a id="385" class="Keyword">import</a> <a id="392" href="Relation.Binary.PreorderReasoning.html" class="Module">Relation.Binary.PreorderReasoning</a> <a id="426" class="Symbol">as</a> <a id="429" class="Module">PreR</a>
<a id="434" class="Keyword">open</a> <a id="439" href="Relation.Binary.PreorderReasoning.html" class="Module">PreR</a> <a id="444" href="Relation.Binary.html#3992" class="Function">preorder</a> <a id="453" class="Keyword">public</a> <a id="460" class="Keyword">renaming</a> <a id="469" class="Symbol">(</a>_∼⟨_⟩_ <a id="477" class="Symbol">to</a> _≤⟨_⟩_<a id="486" class="Symbol">)</a>
</pre></body></html>
|