/usr/share/doc/agda-stdlib-doc/html/Data.Integer.Addition.Properties.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 17 18 19 20 21 22 23 24 25 26 27 28 29 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Integer.Addition.Properties</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">-- Properties related to addition of integers</a>
<a id="152" class="Comment">--</a>
<a id="155" class="Comment">-- This module is DEPRECATED. Please use the corresponding properties in</a>
<a id="228" class="Comment">-- Data.Integer.Properties directly.</a>
<a id="265" class="Comment">------------------------------------------------------------------------</a>
<a id="339" class="Keyword">module</a> <a id="346" href="Data.Integer.Addition.Properties.html" class="Module">Data.Integer.Addition.Properties</a> <a id="379" class="Keyword">where</a>
<a id="386" class="Keyword">open</a> <a id="391" class="Keyword">import</a> <a id="398" href="Data.Integer.Properties.html" class="Module">Data.Integer.Properties</a> <a id="422" class="Keyword">public</a>
<a id="431" class="Keyword">using</a>
<a id="439" class="Symbol">(</a> <a id="441" href="Data.Integer.Properties.html#distrib%CB%A1-%E2%8A%96-%2B-neg" class="Function">distribˡ-⊖-+-neg</a>
<a id="460" class="Symbol">;</a> <a id="462" href="Data.Integer.Properties.html#distrib%CA%B3-%E2%8A%96-%2B-neg" class="Function">distribʳ-⊖-+-neg</a>
<a id="481" class="Symbol">;</a> <a id="483" href="Data.Integer.Properties.html#distrib%CB%A1-%E2%8A%96-%2B-pos" class="Function">distribˡ-⊖-+-pos</a>
<a id="502" class="Symbol">;</a> <a id="504" href="Data.Integer.Properties.html#distrib%CA%B3-%E2%8A%96-%2B-pos" class="Function">distribʳ-⊖-+-pos</a>
<a id="523" class="Symbol">)</a>
<a id="527" class="Keyword">renaming</a>
<a id="538" class="Symbol">(</a> <a id="540" href="Data.Integer.Properties.html#%2B-comm" class="Function">+-comm</a> <a id="564" class="Symbol">to</a> <a id="567" href="Data.Integer.Properties.html#%2B-comm" class="Function">comm</a>
<a id="574" class="Symbol">;</a> <a id="576" href="Data.Integer.Properties.html#%2B-identity%CB%A1" class="Function">+-identityˡ</a> <a id="601" class="Symbol">to</a> <a id="604" href="Data.Integer.Properties.html#%2B-identity%CB%A1" class="Function">identityˡ</a>
<a id="616" class="Symbol">;</a> <a id="618" href="Data.Integer.Properties.html#%2B-identity%CA%B3" class="Function">+-identityʳ</a> <a id="643" class="Symbol">to</a> <a id="646" href="Data.Integer.Properties.html#%2B-identity%CA%B3" class="Function">identityʳ</a>
<a id="658" class="Symbol">;</a> <a id="660" href="Data.Integer.Properties.html#%2B-assoc" class="Function">+-assoc</a> <a id="684" class="Symbol">to</a> <a id="687" href="Data.Integer.Properties.html#%2B-assoc" class="Function">assoc</a>
<a id="695" class="Symbol">;</a> <a id="697" href="Data.Integer.Properties.html#%2B-isSemigroup" class="Function">+-isSemigroup</a> <a id="721" class="Symbol">to</a> <a id="724" href="Data.Integer.Properties.html#%2B-isSemigroup" class="Function">isSemigroup</a>
<a id="738" class="Symbol">;</a> <a id="740" href="Data.Integer.Properties.html#%2B-0-isCommutativeMonoid" class="Function">+-0-isCommutativeMonoid</a> <a id="764" class="Symbol">to</a> <a id="767" href="Data.Integer.Properties.html#%2B-0-isCommutativeMonoid" class="Function">isCommutativeMonoid</a>
<a id="789" class="Symbol">;</a> <a id="791" href="Data.Integer.Properties.html#%2B-0-commutativeMonoid" class="Function">+-0-commutativeMonoid</a> <a id="815" class="Symbol">to</a> <a id="818" href="Data.Integer.Properties.html#%2B-0-commutativeMonoid" class="Function">commutativeMonoid</a>
<a id="838" class="Symbol">)</a>
</pre></body></html>
|