What is the point of giving a POLARITY pragma without any polarities?
E.g. Agda accepts the following without warning:
postulate A : Set
{-# POLARITY A #-}
I think this should be a UselessPragma with deadcode highlighting, and those pragmas should be filtered out by the nicifier.
Consequently, the following would not trigger MultiplePolarityPragmas any more.
Internally, we could represent the collection of those pragmas as a map from names to non-empty lists of polarities.
CC: @nad
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