- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue5043</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--allow-unsolved-metas</a> <a id="36" class="Symbol">#-}</a>
- <a id="latex"></a><a id="41" href="Issue5043.html#41" class="Function">latex</a> <a id="47" class="Symbol">:</a> <a id="49" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="53" href="Issue5043.html#41" class="Function">latex</a> <a id="59" class="Symbol">=</a> <a id="61" class="Hole">{!test!}</a>
- </pre></body></html>
|
