<div dir="ltr"><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Dear all, <br>To kick things off, the first RFC (request for comment) for v2.0 of the Agda standard library is about proposed changes to how numeric operations that require non-zero proofs (e.g. division) work.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><span style="font-weight:600">The current situation</span></p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Currently operations such as division are defined as <a href="https://github.com/agda/agda-stdlib/blob/516c545f28aca931d695a86fbdf7941154b0a64f/src/Data/Nat/DivMod.agda#L43" target="_blank" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/blob/516c545f28aca931d695a86fbdf7941154b0a64f/src/Data/Nat/DivMod.agda#L43" style="color:rgb(0,136,204);text-decoration-line:none">follows</a>:</p><div class="gmail-codehilite" style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none"><pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button class="gmail-btn gmail-pull-left gmail-copy_button_base gmail-copy_codeblock gmail-tippy-zulip-tooltip" aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span class="gmail-nf" style="color:rgb(120,93,161)">_/_</span> <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">:</span> <span class="gmail-o" style="color:rgb(164,29,92)">(</span>dividend divisor <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">:</span> ℕ<span class="gmail-o" style="color:rgb(164,29,92)">)</span> <span class="gmail-o" style="color:rgb(164,29,92)">{</span>≢0 <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">:</span> False <span class="gmail-o" style="color:rgb(164,29,92)">(</span>divisor ≟ <span class="gmail-mi" style="color:rgb(0,133,178)">0</span><span class="gmail-o" style="color:rgb(164,29,92)">)}</span> <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">→</span> ℕ
</code></pre></div><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">taking an implicit proof that the result of the decision procedure of testing whether it is zero reduces to <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">false</code>. This is preferable to passing a direct proof of the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">divisor ≢ 0</code> as it means that when <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">divisor</code> normalises to something of the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">suc n</code> then the type of the proof reduces to unit <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">⊤</code> which Agda automatically fills in. Consequently you can write <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">7 / 3</code> or <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m / </code><span style="color:rgb(0,0,0);font-family:"Source Code Pro",monospace;font-size:11.55px;white-space:pre-wrap">suc</span><code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">n</code> without having to explicitly construct the proof.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><span style="font-weight:600">The current problems</span></p><ol style="padding:0px;margin:0px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><li style="line-height:inherit">When the denominator is not in the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">suc _</code>, Agda can't infer the proof and therefore it must always be passed explicitly even when the proof is in scope. This leads to having to write the ugly code like the following:</li></ol><div class="gmail-codehilite" style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none"><pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button class="gmail-btn gmail-pull-left gmail-copy_button_base gmail-copy_codeblock gmail-tippy-zulip-tooltip" aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">∀</span> m n <span class="gmail-o" style="color:rgb(164,29,92)">{</span>gcd≢0 <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">:</span> NonZero <span class="gmail-o" style="color:rgb(164,29,92)">(</span>gcd m n<span class="gmail-o" style="color:rgb(164,29,92)">)}</span> <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">→</span> Coprime <span class="gmail-o" style="color:rgb(164,29,92)">((</span>m / gcd m n<span class="gmail-o" style="color:rgb(164,29,92)">)</span> <span class="gmail-o" style="color:rgb(164,29,92)">{</span>gcd≢0<span class="gmail-o" style="color:rgb(164,29,92)">})</span> <span class="gmail-o" style="color:rgb(164,29,92)">((</span>n / gcd m n<span class="gmail-o" style="color:rgb(164,29,92)">)</span> <span class="gmail-o" style="color:rgb(164,29,92)">{</span>gcd≢0<span class="gmail-o" style="color:rgb(164,29,92)">})</span>
</code></pre></div><ol start="2" style="padding:0px;margin:2px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><li style="line-height:inherit"><p style="margin:3px 0px">When proving equalities over <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_/_</code> you can't use <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">cong₂</code> from <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Relation.Binary.PropositionalEquality</code> directly as Agda requires that you explicitly prove the proofs of non-zeroness do not affect the result. This makes it very finicky to use equational reasoning.</p></li><li style="line-height:inherit"><p style="margin:3px 0px">The use of the decision procedure <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_≟_</code> means that the definition must depend on <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Properties</code> where <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_≟_</code> lives. This means that a) type-checking anything involving <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_/_</code> requires type-checking a much larger proportion of the library that one would expect and b) <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">_/_</code> can't live in <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Base</code>.</p></li><li style="line-height:inherit"><p style="margin:3px 0px">Constructing a proof of the type <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">False (divisor ≟ 0)</code> is much trickier than a proof of <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">divisor ≢ 0</code>and requires extra imports from <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Relation.Nullary</code>.</p></li></ol><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><span style="font-weight:600">Proposed solution</span></p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">We propose to take a leaf out of Ulf Norell's Prelude library and instead pass the proofs as <em>irrelevant</em>, <em>instance</em> arguments that use the new <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> predicates introduced in v1.5:</p><div class="gmail-codehilite" style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none"><pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button class="gmail-btn gmail-pull-left gmail-copy_button_base gmail-copy_codeblock gmail-tippy-zulip-tooltip" aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span class="gmail-nf" style="color:rgb(120,93,161)">_/_</span> <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">:</span> <span class="gmail-o" style="color:rgb(164,29,92)">(</span>dividend divisor <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">:</span> ℕ<span class="gmail-o" style="color:rgb(164,29,92)">)</span> <span class="gmail-o" style="color:rgb(164,29,92)">{{</span><span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">.</span><span class="gmail-o" style="color:rgb(164,29,92)">(</span>NonZero divisor<span class="gmail-o" style="color:rgb(164,29,92)">)}}</span> <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">→</span> ℕ
</code></pre></div><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">which preserves the ability to not provide the proofs for divisors of the form <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">suc _</code> and fixes the problems listed above as follows:</p><ol style="padding:0px;margin:0px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><li style="line-height:inherit">Agda automatically fills in instance arguments if they are in scope, therefore removing the need to supply them to every place in the expression where they can't be inferred. For example we would then be able to write the much nicer:</li></ol><div class="gmail-codehilite" style="background-image:initial;background-position:0px 0px;background-size:initial;background-repeat:initial;background-origin:initial;background-clip:initial;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px;border:none"><pre style="padding:5px 7px 3px;font-family:"Source Code Pro",monospace;font-size:0.825em;border-radius:4px;margin-top:5px;margin-bottom:5px;line-height:1.4;word-break:break-all;border:1px solid rgba(0,0,0,0.15);direction:ltr;overflow-x:auto"><button class="gmail-btn gmail-pull-left gmail-copy_button_base gmail-copy_codeblock gmail-tippy-zulip-tooltip" aria-label="Copy code" style="font-size:inherit;vertical-align:middle;line-height:11.55px;font-family:"Source Sans 3",sans-serif;float:left;display:block;padding-top:6px;padding-bottom:6px;white-space:nowrap;background-image:none;border-width:initial;border-style:none;border-color:initial;border-radius:0px;height:18px;outline-color:rgb(186,186,186);width:10px;background-clip:content-box"></button><code style="padding:0px;font-family:"Source Code Pro",monospace;font-size:inherit;color:inherit;border-radius:3px;border:0px;white-space:inherit;unicode-bidi:embed;direction:ltr;overflow-x:scroll"><span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">∀</span> m n <span class="gmail-o" style="color:rgb(164,29,92)">{{</span>NonZero <span class="gmail-o" style="color:rgb(164,29,92)">(</span>gcd m n<span class="gmail-o" style="color:rgb(164,29,92)">)}}</span> <span class="gmail-ow" style="color:rgb(165,30,255);font-weight:700">→</span> Coprime <span class="gmail-o" style="color:rgb(164,29,92)">(</span>m / gcd m n<span class="gmail-o" style="color:rgb(164,29,92)">)</span> <span class="gmail-o" style="color:rgb(164,29,92)">(</span>n / gcd m n<span class="gmail-o" style="color:rgb(164,29,92)">)</span>
</code></pre></div><ol start="2" style="padding:0px;margin:2px 0px 5px 20px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><li style="line-height:inherit"><p style="margin:3px 0px">Agda doesn't consider irrelevant arguments when proving propositional equality. Therefore to prove <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m / n</code> and <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">x / y</code> are propositionally equal will only require that we prove <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">m</code> equals <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">x</code> and <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">n</code> equals <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">y</code> and will not require us to explicitly prove that the result doesn't depend on the proofs of non-zeroness.</p></li><li style="line-height:inherit"><p style="margin:3px 0px">The <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> predicate is much more lightweight than the decidability proof and lives in <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Base</code> rather than <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">Data.Nat.Properties</code>.</p></li><li style="line-height:inherit"><p style="margin:3px 0px">The <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> predicate comes with nice constructors <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">nonZero-<</code> and <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">nonZero-≢</code> that makes constructing such proofs much easier.</p></li></ol><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">This has an additional advantage in that for certain operations that always result in a non-zero result, e.g. factorial, it will be possible to declare a proof of the non-zeroness as an instance and you will never have to explicitly pass a proof.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><span style="font-weight:600">Backwards incompatibilities</span></p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">In cases where the proof is already automatically inferred nothing will need to change. In places where the proof has to be passed explicitly, then the type of the proof will need to change and will need to be passed using instance brackets <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">{{_}}</code> rather than implict brackets <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">{_}</code>. As mentioned above, <code style="padding:0px 4px;font-family:"Source Code Pro",monospace;font-size:0.825em;color:rgb(0,0,0);border-radius:3px;border:1px solid rgb(225,225,232);white-space:pre-wrap;unicode-bidi:embed;direction:ltr">NonZero</code> comes with constructors so constructing the new proofs should be much easier.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px"><span style="font-weight:600">Feedback</span></p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Any feedback would be greatly appreciated! Please feel free to reply in one of the following issues:<br><a href="https://github.com/agda/agda-stdlib/issues/921" target="_blank" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues/921" style="color:rgb(0,136,204);text-decoration-line:none">https://github.com/agda/agda-stdlib/issues/921</a><br><a href="https://github.com/agda/agda-stdlib/issues/1170" target="_blank" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues/1170" style="color:rgb(0,136,204);text-decoration-line:none">https://github.com/agda/agda-stdlib/issues/1170</a><br><a href="https://github.com/agda/agda-stdlib/issues/1408" target="_blank" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues/1408" style="color:rgb(0,136,204);text-decoration-line:none">https://github.com/agda/agda-stdlib/issues/1408<br></a></p></div>