| 12345678910111213141516171819202122 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue3965</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">open</a> <a id="6" class="Keyword">import</a> <a id="13" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
- <a id="f"></a><a id="31" href="Issue3965.html#31" class="Function">f</a> <a id="33" class="Symbol">:</a> <a id="35" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a> <a id="39" class="Symbol">→</a> <a id="41" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a>
- <a id="45" href="Issue3965.html#31" class="Function">f</a> <a id="47" class="Number">0</a> <a id="49" class="Symbol">=</a> <a id="51" href="Agda.Builtin.Nat.html#195" class="InductiveConstructor">zero</a>
- <a id="56" href="Issue3965.html#31" class="Deadcode Function">f</a><a id="57" class="Deadcode"> </a><a id="58" class="Deadcode Number">0</a><a id="59" class="Deadcode"> </a><a id="60" class="Deadcode Symbol">=</a><a id="61" class="Deadcode"> </a><a id="62" class="Deadcode Number">0</a> <a id="71" class="Comment">-- All -- But Only</a>
- <a id="111" href="Issue3965.html#31" class="Function">f</a> <a id="113" class="Symbol">(</a><a id="114" href="Agda.Builtin.Nat.html#208" class="InductiveConstructor">suc</a> <a id="118" href="Issue3965.html#118" class="Bound">n</a><a id="119" class="Symbol">)</a> <a id="121" class="Symbol">=</a> <a id="123" href="Issue3965.html#118" class="Bound">n</a> <a id="126" class="Comment">-- These</a>
- <a id="135" href="Issue3965.html#31" class="Deadcode Function">f</a><a id="136" class="Deadcode"> </a><a id="137" class="Deadcode Number">0</a><a id="138" class="Deadcode"> </a><a id="139" class="Deadcode Symbol">=</a><a id="140" class="Deadcode"> </a><a id="141" class="Deadcode Number">0</a> <a id="150" class="Comment">-- Lines -- These Two</a>
- <a id="206" class="Comment">-- Used to be highlighted -- Should be!</a>
- <a id="g"></a><a id="250" href="Issue3965.html#250" class="Function">g</a> <a id="252" class="Symbol">:</a> <a id="254" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a> <a id="258" class="Symbol">→</a> <a id="260" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a>
- <a id="264" href="Issue3965.html#250" class="Function">g</a> <a id="266" class="Number">0</a> <a id="268" class="Symbol">=</a> <a id="270" href="Agda.Builtin.Nat.html#195" class="InductiveConstructor">zero</a>
- <a id="275" href="Issue3965.html#250" class="Deadcode Function">g</a><a id="276" class="Deadcode"> </a><a id="277" class="Deadcode Number">0</a><a id="278" class="Deadcode"> </a><a id="283" class="Deadcode Comment">-- The highlihting should still</a><a id="314" class="Deadcode">
- </a><a id="317" class="Deadcode Symbol">=</a><a id="318" class="Deadcode"> </a><a id="319" class="Deadcode Number">0</a> <a id="323" class="Comment">-- span multiple lines if the clause does</a>
- <a id="365" href="Issue3965.html#250" class="Function">g</a> <a id="367" class="Symbol">(</a><a id="368" href="Agda.Builtin.Nat.html#208" class="InductiveConstructor">suc</a> <a id="372" href="Issue3965.html#372" class="Bound">n</a><a id="373" class="Symbol">)</a> <a id="375" class="Symbol">=</a> <a id="377" href="Issue3965.html#372" class="Bound">n</a>
- <a id="379" href="Issue3965.html#250" class="Deadcode Function">g</a><a id="380" class="Deadcode"> </a><a id="381" class="Deadcode Number">0</a><a id="382" class="Deadcode"> </a><a id="387" class="Deadcode Comment">-- Even</a><a id="394" class="Deadcode">
- </a><a id="403" class="Deadcode Comment">-- With</a><a id="410" class="Deadcode">
- </a><a id="419" class="Deadcode Comment">-- A Lot</a><a id="427" class="Deadcode">
- </a><a id="431" class="Deadcode Symbol">=</a><a id="432" class="Deadcode"> </a><a id="433" class="Deadcode Number">0</a> <a id="436" class="Comment">-- Of Empty Lines in between</a>
- </pre></body></html>
|
