In the following code the warning NotAffectedByOpaque is turned off, and Agda does not print any warning, but the definition of R is still highlighted with agda2-highlight-deadcode-face:
{-# OPTIONS -WnoNotAffectedByOpaque #-}
opaque
record R : Set where
r : R
r = record {}
Similarly, in the following code the warning UselessOpaque is turned off, and Agda does not print any warning, but the opaque keyword is still highlighted with agda2-highlight-deadcode-face:
{-# OPTIONS -WnoUselessOpaque #-}
opaque
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