In generated HTML, macro names (for example, the 1lab's Regularity.reduce! macro) have class Function at definition site but Macro at use site (e.g. here). Also, there's no rule for .Macro in the default style sheet, so they end up having the browser's default colour for links. (fixed)
Reproducer:
open import Agda.Builtin.List open import Agda.Builtin.Reflection open import Agda.Builtin.Unit macro bug : Term → TC ⊤ bug h = unify h (quoteTerm tt) _ = bug
I can't really tell how the highlighter works but this line looks suspicious as it discards the DefInfo containing defMacro:
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