Since #7613, the following file
module bug where module X where module _ (a : Set) (let module Y = X) where
produces the following HTML
<!DOCTYPE HTML> <html><head><meta charset="utf-8"><title>bug</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="bug.html" class="Module">bug</a> <a id="12" class="Keyword">where</a> <a id="18" class="Keyword">module</a> <a id="X"></a><a id="25" href="bug.html#25" class="Module">X</a> <a id="27" class="Keyword">where</a> <a id="33" class="Keyword">module</a> <a id="40" href="bug.html#40" class="Module">_</a> <a id="44" class="Symbol">(</a>a <a id="47" class="Symbol">:</a> Set<a id="52" class="Symbol">)</a> <a id="56" class="Symbol">(</a><a id="57" class="Keyword">let</a> <a id="61" class="Keyword">module</a> <a id="68" href="bug.html#68" class="Module">Y</a> <a id="70" class="Symbol">=</a> <a id="72" href="bug.html#25" class="Module">X</a><a id="73" class="Symbol">)</a> <a id="77" class="Keyword">where</a> </pre></body></html>
Note that a and Set are not highlighted: the expected output for line 5 is
<a id="44" class="Symbol">(</a><a id="45" href="bug.html#45" class="Bound">a</a> <a id="47" class="Symbol">:</a> <a id="49" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="52" class="Symbol">)</a>
This only happens to arguments before the let module.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4