Deploying to gh-pages from @ 3c6c47c 🚀

master/Algebra.Properties.Semiring.Exp.TCOptimised.html

@@ -44,5 +44,5 @@
 
 <a id="1411" class="Comment">-- (xᵐ)ⁿ≈xᵐ*ⁿ</a>
 <a id="^-assocʳ"></a><a id="1425" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1425" class="Function">^-assocʳ</a> <a id="1434" class="Symbol">:</a> <a id="1436" class="Symbol">∀</a> <a id="1438" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1438" class="Bound">x</a> <a id="1440" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1440" class="Bound">m</a> <a id="1442" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1442" class="Bound">n</a> <a id="1444" class="Symbol">→</a> <a id="1446" class="Symbol">(</a><a id="1447" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1438" class="Bound">x</a> <a id="1449" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1069" class="Function Operator">^</a> <a id="1451" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1440" class="Bound">m</a><a id="1452" class="Symbol">)</a> <a id="1454" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1069" class="Function Operator">^</a> <a id="1456" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1442" class="Bound">n</a> <a id="1458" href="Algebra.Bundles.html#18574" class="Field Operator">≈</a> <a id="1460" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1438" class="Bound">x</a> <a id="1462" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1069" class="Function Operator">^</a> <a id="1464" class="Symbol">(</a><a id="1465" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1440" class="Bound">m</a> <a id="1467" href="Agda.Builtin.Nat.html#539" class="Primitive Operator">ℕ.*</a> <a id="1471" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1442" class="Bound">n</a><a id="1472" class="Symbol">)</a>
-<a id="1474" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1425" class="Function">^-assocʳ</a> <a id="1483" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1483" class="Bound">x</a> <a id="1485" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">m</a> <a id="1487" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">n</a> <a id="1489" class="Keyword">rewrite</a> <a id="1497" href="Data.Nat.Properties.html#21920" class="Function">ℕ.*-comm</a> <a id="1506" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">m</a> <a id="1508" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">n</a> <a id="1510" class="Symbol">=</a> <a id="1512" href="Algebra.Properties.Monoid.Mult.TCOptimised.html#2363" class="Function">Mult.×-assocˡ</a> <a id="1526" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1483" class="Bound">x</a> <a id="1528" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">n</a> <a id="1530" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">m</a>
+<a id="1474" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1425" class="Function">^-assocʳ</a> <a id="1483" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1483" class="Bound">x</a> <a id="1485" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">m</a> <a id="1487" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">n</a> <a id="1489" class="Keyword">rewrite</a> <a id="1497" href="Data.Nat.Properties.html#21984" class="Function">ℕ.*-comm</a> <a id="1506" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">m</a> <a id="1508" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">n</a> <a id="1510" class="Symbol">=</a> <a id="1512" href="Algebra.Properties.Monoid.Mult.TCOptimised.html#2363" class="Function">Mult.×-assocˡ</a> <a id="1526" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1483" class="Bound">x</a> <a id="1528" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1487" class="Bound">n</a> <a id="1530" href="Algebra.Properties.Semiring.Exp.TCOptimised.html#1485" class="Bound">m</a>
 </pre></body></html>

master/Algebra.Properties.Semiring.Exp.html

@@ -44,7 +44,7 @@
 
 <a id="1305" class="Comment">-- (xᵐ)ⁿ≈xᵐ*ⁿ</a>
 <a id="^-assocʳ"></a><a id="1319" href="Algebra.Properties.Semiring.Exp.html#1319" class="Function">^-assocʳ</a> <a id="1328" class="Symbol">:</a> <a id="1330" class="Symbol">∀</a> <a id="1332" href="Algebra.Properties.Semiring.Exp.html#1332" class="Bound">x</a> <a id="1334" href="Algebra.Properties.Semiring.Exp.html#1334" class="Bound">m</a> <a id="1336" href="Algebra.Properties.Semiring.Exp.html#1336" class="Bound">n</a> <a id="1338" class="Symbol">→</a> <a id="1340" class="Symbol">(</a><a id="1341" href="Algebra.Properties.Semiring.Exp.html#1332" class="Bound">x</a> <a id="1343" href="Algebra.Definitions.RawSemiring.html#1256" class="Function Operator">^</a> <a id="1345" href="Algebra.Properties.Semiring.Exp.html#1334" class="Bound">m</a><a id="1346" class="Symbol">)</a> <a id="1348" href="Algebra.Definitions.RawSemiring.html#1256" class="Function Operator">^</a> <a id="1350" href="Algebra.Properties.Semiring.Exp.html#1336" class="Bound">n</a> <a id="1352" href="Algebra.Bundles.html#18574" class="Field Operator">≈</a> <a id="1354" href="Algebra.Properties.Semiring.Exp.html#1332" class="Bound">x</a> <a id="1356" href="Algebra.Definitions.RawSemiring.html#1256" class="Function Operator">^</a> <a id="1358" class="Symbol">(</a><a id="1359" href="Algebra.Properties.Semiring.Exp.html#1334" class="Bound">m</a> <a id="1361" href="Agda.Builtin.Nat.html#539" class="Primitive Operator">ℕ.*</a> <a id="1365" href="Algebra.Properties.Semiring.Exp.html#1336" class="Bound">n</a><a id="1366" class="Symbol">)</a>
-<a id="1368" href="Algebra.Properties.Semiring.Exp.html#1319" class="Function">^-assocʳ</a> <a id="1377" href="Algebra.Properties.Semiring.Exp.html#1377" class="Bound">x</a> <a id="1379" href="Algebra.Properties.Semiring.Exp.html#1379" class="Bound">m</a> <a id="1381" href="Algebra.Properties.Semiring.Exp.html#1381" class="Bound">n</a> <a id="1383" class="Keyword">rewrite</a> <a id="1391" href="Data.Nat.Properties.html#21920" class="Function">ℕ.*-comm</a> <a id="1400" href="Algebra.Properties.Semiring.Exp.html#1379" class="Bound">m</a> <a id="1402" href="Algebra.Properties.Semiring.Exp.html#1381" class="Bound">n</a> <a id="1404" class="Symbol">=</a> <a id="1406" href="Algebra.Properties.Monoid.Mult.html#2173" class="Function">Mult.×-assocˡ</a> <a id="1420" href="Algebra.Properties.Semiring.Exp.html#1377" class="Bound">x</a> <a id="1422" href="Algebra.Properties.Semiring.Exp.html#1381" class="Bound">n</a> <a id="1424" href="Algebra.Properties.Semiring.Exp.html#1379" class="Bound">m</a>
+<a id="1368" href="Algebra.Properties.Semiring.Exp.html#1319" class="Function">^-assocʳ</a> <a id="1377" href="Algebra.Properties.Semiring.Exp.html#1377" class="Bound">x</a> <a id="1379" href="Algebra.Properties.Semiring.Exp.html#1379" class="Bound">m</a> <a id="1381" href="Algebra.Properties.Semiring.Exp.html#1381" class="Bound">n</a> <a id="1383" class="Keyword">rewrite</a> <a id="1391" href="Data.Nat.Properties.html#21984" class="Function">ℕ.*-comm</a> <a id="1400" href="Algebra.Properties.Semiring.Exp.html#1379" class="Bound">m</a> <a id="1402" href="Algebra.Properties.Semiring.Exp.html#1381" class="Bound">n</a> <a id="1404" class="Symbol">=</a> <a id="1406" href="Algebra.Properties.Monoid.Mult.html#2173" class="Function">Mult.×-assocˡ</a> <a id="1420" href="Algebra.Properties.Semiring.Exp.html#1377" class="Bound">x</a> <a id="1422" href="Algebra.Properties.Semiring.Exp.html#1381" class="Bound">n</a> <a id="1424" href="Algebra.Properties.Semiring.Exp.html#1379" class="Bound">m</a>
 
 <a id="1427" class="Comment">------------------------------------------------------------------------</a>
 <a id="1500" class="Comment">-- A lemma using commutativity, needed for the Binomial Theorem</a>

master/Algebra.Solver.CommutativeMonoid.html

@@ -177,7 +177,7 @@
 <a id="4998" class="Keyword">infix</a> <a id="5004" class="Number">5</a> <a id="5006" href="Algebra.Solver.CommutativeMonoid.html#5011" class="Function Operator">_≟_</a>
 
 <a id="_≟_"></a><a id="5011" href="Algebra.Solver.CommutativeMonoid.html#5011" class="Function Operator">_≟_</a> <a id="5015" class="Symbol">:</a> <a id="5017" class="Symbol">(</a><a id="5018" href="Algebra.Solver.CommutativeMonoid.html#5018" class="Bound">nf₁</a> <a id="5022" href="Algebra.Solver.CommutativeMonoid.html#5022" class="Bound">nf₂</a> <a id="5026" class="Symbol">:</a> <a id="5028" href="Algebra.Solver.CommutativeMonoid.html#2012" class="Function">Normal</a> <a id="5035" href="Algebra.Solver.CommutativeMonoid.html#1227" class="Generalizable">n</a><a id="5036" class="Symbol">)</a> <a id="5038" class="Symbol">→</a> <a id="5040" href="Relation.Nullary.Decidable.Core.html#1667" class="Record">Dec</a> <a id="5044" class="Symbol">(</a><a id="5045" href="Algebra.Solver.CommutativeMonoid.html#5018" class="Bound">nf₁</a> <a id="5049" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="5051" href="Algebra.Solver.CommutativeMonoid.html#5022" class="Bound">nf₂</a><a id="5054" class="Symbol">)</a>
-<a id="5056" href="Algebra.Solver.CommutativeMonoid.html#5056" class="Bound">nf₁</a> <a id="5060" href="Algebra.Solver.CommutativeMonoid.html#5011" class="Function Operator">≟</a> <a id="5062" href="Algebra.Solver.CommutativeMonoid.html#5062" class="Bound">nf₂</a> <a id="5066" class="Symbol">=</a> <a id="5068" href="Relation.Nullary.Decidable.html#1241" class="Function">Dec.map</a> <a id="5076" href="Data.Vec.Relation.Binary.Pointwise.Inductive.html#9718" class="Function">Pointwise-≡↔≡</a> <a id="5090" class="Symbol">(</a><a id="5091" href="Data.Vec.Relation.Binary.Pointwise.Inductive.html#3736" class="Function">decidable</a> <a id="5101" href="Data.Nat.Properties.html#3810" class="Function Operator">ℕ._≟_</a> <a id="5107" href="Algebra.Solver.CommutativeMonoid.html#5056" class="Bound">nf₁</a> <a id="5111" href="Algebra.Solver.CommutativeMonoid.html#5062" class="Bound">nf₂</a><a id="5114" class="Symbol">)</a>
+<a id="5056" href="Algebra.Solver.CommutativeMonoid.html#5056" class="Bound">nf₁</a> <a id="5060" href="Algebra.Solver.CommutativeMonoid.html#5011" class="Function Operator">≟</a> <a id="5062" href="Algebra.Solver.CommutativeMonoid.html#5062" class="Bound">nf₂</a> <a id="5066" class="Symbol">=</a> <a id="5068" href="Relation.Nullary.Decidable.html#1241" class="Function">Dec.map</a> <a id="5076" href="Data.Vec.Relation.Binary.Pointwise.Inductive.html#9718" class="Function">Pointwise-≡↔≡</a> <a id="5090" class="Symbol">(</a><a id="5091" href="Data.Vec.Relation.Binary.Pointwise.Inductive.html#3736" class="Function">decidable</a> <a id="5101" href="Data.Nat.Properties.html#3874" class="Function Operator">ℕ._≟_</a> <a id="5107" href="Algebra.Solver.CommutativeMonoid.html#5056" class="Bound">nf₁</a> <a id="5111" href="Algebra.Solver.CommutativeMonoid.html#5062" class="Bound">nf₂</a><a id="5114" class="Symbol">)</a>
   <a id="5118" class="Keyword">where</a> <a id="5124" class="Keyword">open</a> <a id="5129" href="Data.Vec.Relation.Binary.Pointwise.Inductive.html" class="Module">Pointwise</a>
 
 <a id="5140" class="Comment">-- We can also give a sound, but not necessarily complete, procedure</a>

master/Algebra.Solver.Ring.NaturalCoefficients.Default.html

@@ -19,7 +19,7 @@
 
 <a id="622" class="Keyword">import</a> <a id="629" href="Algebra.Properties.Semiring.Mult.html" class="Module">Algebra.Properties.Semiring.Mult</a> <a id="662" class="Symbol">as</a> <a id="665" class="Module">SemiringMultiplication</a>
 <a id="688" class="Keyword">open</a> <a id="693" class="Keyword">import</a> <a id="700" href="Data.Maybe.Base.html" class="Module">Data.Maybe.Base</a> <a id="716" class="Keyword">using</a> <a id="722" class="Symbol">(</a><a id="723" href="Agda.Builtin.Maybe.html#135" class="Datatype">Maybe</a><a id="728" class="Symbol">;</a> <a id="730" href="Data.Maybe.Base.html#2110" class="Function">map</a><a id="733" class="Symbol">)</a>
-<a id="735" class="Keyword">open</a> <a id="740" class="Keyword">import</a> <a id="747" href="Data.Nat.html" class="Module">Data.Nat</a> <a id="756" class="Keyword">using</a> <a id="762" class="Symbol">(</a><a id="763" href="Data.Nat.Properties.html#3810" class="Function Operator">_≟_</a><a id="766" class="Symbol">)</a>
+<a id="735" class="Keyword">open</a> <a id="740" class="Keyword">import</a> <a id="747" href="Data.Nat.html" class="Module">Data.Nat</a> <a id="756" class="Keyword">using</a> <a id="762" class="Symbol">(</a><a id="763" href="Data.Nat.Properties.html#3874" class="Function Operator">_≟_</a><a id="766" class="Symbol">)</a>
 <a id="768" class="Keyword">open</a> <a id="773" class="Keyword">import</a> <a id="780" href="Relation.Binary.Consequences.html" class="Module">Relation.Binary.Consequences</a> <a id="809" class="Keyword">using</a> <a id="815" class="Symbol">(</a><a id="816" href="Relation.Binary.Consequences.html#6955" class="Function">dec⇒weaklyDec</a><a id="829" class="Symbol">)</a>
 <a id="831" class="Keyword">import</a> <a id="838" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="881" class="Symbol">as</a> <a id="884" class="Module">≡</a>
 
@@ -28,7 +28,7 @@
 
 <a id="952" class="Keyword">private</a>
   <a id="dec"></a><a id="962" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#962" class="Function">dec</a> <a id="966" class="Symbol">:</a> <a id="968" class="Symbol">∀</a> <a id="970" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#970" class="Bound">m</a> <a id="972" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#972" class="Bound">n</a> <a id="974" class="Symbol">→</a> <a id="976" href="Agda.Builtin.Maybe.html#135" class="Datatype">Maybe</a> <a id="982" class="Symbol">(</a><a id="983" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#970" class="Bound">m</a> <a id="985" href="Algebra.Definitions.RawMonoid.html#1089" class="Function Operator">×</a> <a id="987" href="Algebra.Bundles.html#19879" class="Field">1#</a> <a id="990" href="Algebra.Bundles.html#19721" class="Field Operator">≈</a> <a id="992" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#972" class="Bound">n</a> <a id="994" href="Algebra.Definitions.RawMonoid.html#1089" class="Function Operator">×</a> <a id="996" href="Algebra.Bundles.html#19879" class="Field">1#</a><a id="998" class="Symbol">)</a>
-  <a id="1002" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#962" class="Function">dec</a> <a id="1006" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1006" class="Bound">m</a> <a id="1008" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1008" class="Bound">n</a> <a id="1010" class="Symbol">=</a> <a id="1012" href="Data.Maybe.Base.html#2110" class="Function">map</a> <a id="1016" class="Symbol">(λ</a> <a id="1019" class="Symbol">{</a> <a id="1021" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">≡.refl</a> <a id="1028" class="Symbol">→</a> <a id="1030" href="Relation.Binary.Structures.html#1596" class="Function">refl</a> <a id="1035" class="Symbol">})</a> <a id="1038" class="Symbol">(</a><a id="1039" href="Relation.Binary.Consequences.html#6955" class="Function">dec⇒weaklyDec</a> <a id="1053" href="Data.Nat.Properties.html#3810" class="Function Operator">_≟_</a> <a id="1057" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1006" class="Bound">m</a> <a id="1059" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1008" class="Bound">n</a><a id="1060" class="Symbol">)</a>
+  <a id="1002" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#962" class="Function">dec</a> <a id="1006" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1006" class="Bound">m</a> <a id="1008" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1008" class="Bound">n</a> <a id="1010" class="Symbol">=</a> <a id="1012" href="Data.Maybe.Base.html#2110" class="Function">map</a> <a id="1016" class="Symbol">(λ</a> <a id="1019" class="Symbol">{</a> <a id="1021" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">≡.refl</a> <a id="1028" class="Symbol">→</a> <a id="1030" href="Relation.Binary.Structures.html#1596" class="Function">refl</a> <a id="1035" class="Symbol">})</a> <a id="1038" class="Symbol">(</a><a id="1039" href="Relation.Binary.Consequences.html#6955" class="Function">dec⇒weaklyDec</a> <a id="1053" href="Data.Nat.Properties.html#3874" class="Function Operator">_≟_</a> <a id="1057" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1006" class="Bound">m</a> <a id="1059" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#1008" class="Bound">n</a><a id="1060" class="Symbol">)</a>
 
 <a id="1063" class="Keyword">open</a> <a id="1068" class="Keyword">import</a> <a id="1075" href="Algebra.Solver.Ring.NaturalCoefficients.html" class="Module">Algebra.Solver.Ring.NaturalCoefficients</a> <a id="1115" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#584" class="Bound">R</a> <a id="1117" href="Algebra.Solver.Ring.NaturalCoefficients.Default.html#962" class="Function">dec</a> <a id="1121" class="Keyword">public</a>
 </pre></body></html>