Deploying to main from @ anoma/nspec@0887f4c 🚀

Author: vveiln

pr-390/404.html

@@ -146,7 +146,7 @@
                 <span class="first-letter">s</span>pecs
 
 
-                <span class="md-header__topic-version">(PR390 - yulia/shielded-spec-763e9964)</span>
+                <span class="md-header__topic-version">(PR390 - yulia/shielded-spec-0887f4c6)</span>
 
             </span>
           </div>
@@ -334,7 +334,7 @@
         class="md-nav__link"
         target="_blank"
       >
-     Latest version ((PR390 - yulia/shielded-spec-763e9964))
+     Latest version ((PR390 - yulia/shielded-spec-0887f4c6))
       </a>
     </li>
     <li class="md-nav__item">
@@ -1080,8 +1080,8 @@ <h1>404 - Not found</h1>
       Powered by Mkdocs, Poetry , Material 9.6.12-insiders-4.53.16 and Juvix v0.6.10
     </div>
 
-  <strong>Version: (PR390 - yulia/shielded-spec-763e9964) - Updated: October 14,
-    2025 at 01:06 PM UTC</strong> 
+  <strong>Version: (PR390 - yulia/shielded-spec-0887f4c6) - Updated: October 17,
+    2025 at 08:57 AM UTC</strong> 
   <br/>
   <strong>Latest version: <a href="https://specs.anoma.net/latest">
     https://specs.anoma.net/latest</a></strong>

pr-390/Juvix/Builtin/V1/Bool-src.html

@@ -8,4 +8,4 @@
   <span class="ju-keyword">|</span> <span id="Bool.true"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Bool-src.html#Bool.true" class="ju-code-link ju-constructor"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Bool-src.html#Bool.true" class="ju-code-link ju-constructor"><span class="ju-constructor">true</span></a></span></a></span></span><span class="ju-delimiter">;</span>
 
 <span class="ju-keyword">open</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Bool-src.html#Bool" class="ju-code-link ju-module"><span class="ju-module">Bool</span></a></span> <span class="ju-keyword">using</span> <span class="ju-delimiter">{</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Bool-src.html#Bool.false" class="ju-code-link ju-constructor"><span class="ju-constructor">false</span></a></span><span class="ju-delimiter">;</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Bool-src.html#Bool.true" class="ju-code-link ju-constructor"><span class="ju-constructor">true</span></a></span><span class="ju-delimiter">}</span> <span class="ju-keyword">public</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/Fixity-src.html

@@ -26,4 +26,4 @@
 
 <span class="ju-keyword">syntax</span> <span class="ju-keyword">fixity</span> <span class="ju-fixity"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Fixity-src.html#composition" class="ju-code-link ju-fixity"><span class="ju-fixity">composition</span></a></span></span> <span class="ju-keyword">:=</span> binary <span class="ju-delimiter">{</span><span class="ju-keyword">assoc</span> <span class="ju-keyword">:=</span> right<span class="ju-delimiter">;</span> <span class="ju-keyword">above</span> <span class="ju-keyword">:=</span> <span class="ju-delimiter">[</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Fixity-src.html#multiplicative" class="ju-code-link ju-fixity"><span class="ju-fixity">multiplicative</span></a></span><span class="ju-delimiter">]</span><span class="ju-delimiter">}</span><span class="ju-delimiter">;</span>
 <span class="ju-keyword">syntax</span> <span class="ju-keyword">fixity</span> <span class="ju-fixity"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Fixity-src.html#lcomposition" class="ju-code-link ju-fixity"><span class="ju-fixity">lcomposition</span></a></span></span> <span class="ju-keyword">:=</span> binary <span class="ju-delimiter">{</span><span class="ju-keyword">assoc</span> <span class="ju-keyword">:=</span> left<span class="ju-delimiter">;</span> <span class="ju-keyword">above</span> <span class="ju-keyword">:=</span> <span class="ju-delimiter">[</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Fixity-src.html#multiplicative" class="ju-code-link ju-fixity"><span class="ju-fixity">multiplicative</span></a></span><span class="ju-delimiter">]</span><span class="ju-delimiter">}</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/List-src.html

@@ -14,4 +14,4 @@
     <span id="List.::"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#List.::" class="ju-code-link ju-constructor"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#List.::" class="ju-code-link ju-constructor"><span class="ju-constructor">::</span></a></span></a></span></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#Juvix.Builtin.V1.List:5" class="ju-code-link ju-var"><span class="ju-var">A</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#List" class="ju-code-link ju-inductive"><span class="ju-inductive"><span class="ju-delimiter">(</span>List</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#Juvix.Builtin.V1.List:5" class="ju-code-link ju-var"><span class="ju-var">A</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span>
 
 <span class="ju-keyword">open</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#List" class="ju-code-link ju-module"><span class="ju-module">List</span></a></span> <span class="ju-keyword">using</span> <span class="ju-delimiter">{</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#List.nil" class="ju-code-link ju-constructor"><span class="ju-constructor">nil</span></a></span><span class="ju-delimiter">;</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/List-src.html#List.::" class="ju-code-link ju-constructor"><span class="ju-constructor">::</span></a></span><span class="ju-delimiter">}</span> <span class="ju-keyword">public</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/Maybe-src.html

@@ -9,4 +9,4 @@
   <span class="ju-keyword">|</span> <span id="Maybe.just"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Maybe-src.html#Maybe.just" class="ju-code-link ju-constructor"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Maybe-src.html#Maybe.just" class="ju-code-link ju-constructor"><span class="ju-constructor">just</span></a></span></a></span></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Maybe-src.html#Juvix.Builtin.V1.Maybe:5" class="ju-code-link ju-var"><span class="ju-var">A</span></a></span><span class="ju-delimiter">;</span>
 
 <span class="ju-keyword">open</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Maybe-src.html#Maybe" class="ju-code-link ju-module"><span class="ju-module">Maybe</span></a></span> <span class="ju-keyword">using</span> <span class="ju-delimiter">{</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Maybe-src.html#Maybe.nothing" class="ju-code-link ju-constructor"><span class="ju-constructor">nothing</span></a></span><span class="ju-delimiter">;</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Maybe-src.html#Maybe.just" class="ju-code-link ju-constructor"><span class="ju-constructor">just</span></a></span><span class="ju-delimiter">}</span> <span class="ju-keyword">public</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/Nat-src.html

@@ -20,4 +20,4 @@
     <span id="Juvix.Builtin.V1.Nat:5"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat-src.html#Juvix.Builtin.V1.Nat:5" class="ju-code-link ju-function"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat-src.html#Juvix.Builtin.V1.Nat:5" class="ju-code-link ju-function"><span class="ju-function">+</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#+" class="ju-code-link ju-function"><span class="ju-function"><span class="ju-delimiter">(</span>Nat<span class="ju-delimiter">.</span>+</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span>
     <span id="Juvix.Builtin.V1.Nat:6"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat-src.html#Juvix.Builtin.V1.Nat:6" class="ju-code-link ju-function"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat-src.html#Juvix.Builtin.V1.Nat:6" class="ju-code-link ju-function"><span class="ju-function">*</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#*" class="ju-code-link ju-function"><span class="ju-function"><span class="ju-delimiter">(</span>Nat<span class="ju-delimiter">.</span>*</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span>
   <span class="ju-delimiter">}</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/Nat/Base-src.html

@@ -48,4 +48,4 @@
 <span class="ju-judoc">---</span> <span class="ju-judoc">Modulo for </span><span class="ju-judoc">;</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Nat" class="ju-code-link ju-inductive"><span class="ju-inductive">Nat</span></a></span><span class="ju-judoc">;</span><span class="ju-judoc">s.</span>
 <span class="ju-keyword">builtin</span> <span class="ju-keyword">nat-mod</span>
 <span id="mod"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#mod" class="ju-code-link ju-function"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#mod" class="ju-code-link ju-function"><span class="ju-function">mod</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Juvix.Builtin.V1.Nat.Base:23" class="ju-code-link ju-var"><span class="ju-var">n</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Juvix.Builtin.V1.Nat.Base:24" class="ju-code-link ju-var"><span class="ju-var">m</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Nat" class="ju-code-link ju-inductive"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Nat" class="ju-code-link ju-inductive"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#sub" class="ju-code-link ju-function"><span class="ju-function">sub</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Juvix.Builtin.V1.Nat.Base:23" class="ju-code-link ju-var"><span class="ju-var">n</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#div" class="ju-code-link ju-function"><span class="ju-function"><span class="ju-delimiter">(</span>div</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Juvix.Builtin.V1.Nat.Base:23" class="ju-code-link ju-var"><span class="ju-var">n</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Juvix.Builtin.V1.Nat.Base:24" class="ju-code-link ju-var"><span class="ju-var">m</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#*" class="ju-code-link ju-function"><span class="ju-function">*</span></a></span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Nat/Base-src.html#Juvix.Builtin.V1.Nat.Base:24" class="ju-code-link ju-var"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/String-src.html

@@ -11,4 +11,4 @@
 <span class="ju-judoc">---</span> <span class="ju-judoc">Concatenation of two </span><span class="ju-judoc">;</span><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/String-src.html#String" class="ju-code-link ju-inductive"><span class="ju-axiom">String</span></a></span><span class="ju-judoc">;</span><span class="ju-judoc">s.</span>
 <span class="ju-keyword">builtin</span> <span class="ju-keyword">string-concat</span>
 <span class="ju-keyword">axiom</span> <span id="++str"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/String-src.html#++str" class="ju-code-link ju-function"><span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/String-src.html#++str" class="ju-code-link ju-function"><span class="ju-axiom">++str</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/String-src.html#String" class="ju-code-link ju-inductive"><span class="ju-axiom">String</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/String-src.html#String" class="ju-code-link ju-inductive"><span class="ju-axiom">String</span></a></span> <span class="ju-keyword">-&gt;</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/String-src.html#String" class="ju-code-link ju-inductive"><span class="ju-axiom">String</span></a></span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/Trait/FromNatural-src.html

@@ -11,4 +11,4 @@
   <span class="ju-delimiter">}</span><span class="ju-delimiter">;</span>
 
 <span class="ju-keyword">open</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Trait/FromNatural-src.html#FromNatural" class="ju-code-link ju-module"><span class="ju-module">FromNatural</span></a></span> <span class="ju-keyword">public</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>

pr-390/Juvix/Builtin/V1/Trait/Natural-src.html

@@ -18,4 +18,4 @@
   <span class="ju-delimiter">}</span><span class="ju-delimiter">;</span>
 
 <span class="ju-keyword">open</span> <span class="annot"><a href="https://specs.anoma.net/pr-390/Juvix/Builtin/V1/Trait/Natural-src.html#Natural" class="ju-code-link ju-module"><span class="ju-module">Natural</span></a></span> <span class="ju-keyword">public</span><span class="ju-delimiter">;</span>
-</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-14 13:06 UTC</pre></footer></html>
+</pre><footer><pre>Powered by <a href="https://juvix.org">Juvix </a><a href="https://github.com/anoma/juvix/commit/b935467">0.6.10-b935467</a></pre></footer><footer><pre>Last modified on 2025-10-17 8:57 UTC</pre></footer></html>