not package:Agda
Outside of any opaque blocks.
This note, if not null, can be displayed as a tool-tip or something
like that. It should contain useful information about the range (like
the module containing a certain identifier, or the fixity of an
operator).
Associativity and precedence (fixity) of the names.
True if the notation comes from an operator (rather than a syntax
declaration).
The names the syntax and/or fixity belong to.
Invariant: The set is non-empty. Every name in the list matches
notaName.
Syntax associated with the names.
Classify a notation by presence of leading and/or trailing
normal holes.
Return the
IdParts of a notation, the first part qualified, the
other parts unqualified. This allows for qualified use of operators,
e.g.,
M.for x ∈ xs return e, or
x ℕ.+ y.
Project name of unshadowed local variable.
Get all locals that are not shadowed by imports.