fix package:Agda

Range of the whole fixity declaration.

Get the fixities and polarity pragmas from the current block. Doesn't go inside modules and where blocks. The reason for this is that these declarations have to appear at the same level (or possibly outside an abstract or mutual block) as their target declaration.

Fixity of modules cannot be changed via renaming (since modules have no fixity).

Fixity of operators.

The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.

Collecting fixity declarations (and polarity pragmas) for concrete declarations.

Definitions for fixity, precedence levels, and declared syntax.

Should system generated projections ProjSystem be printed postfix (True) or prefix (False).