Agda.Syntax.Common.Aspect

Symbols like forall, =, ->, etc.

Things like Set and Prop.

Is the name an operator part?

Text occurring in pragmas that does not have a more specific aspect.

Non-code contents in literate Agda

Delimiters used to separate the Agda code blocks from the other contents in literate Agda

Bound variable.

Generalizable variable. (This includes generalizable variables that have been generalized).

Inductive or coinductive constructor.

Record field.

Module name.

Primitive.

Record type.

Named argument, like x in {x = v}

Macro.

A warning that is considered fatal in the end.

Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.

Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc.

Used for shadowed repeated variable names in telescopes.

When this constructor is used it is probably a good idea to include a note explaining why the pattern is incomplete.

Code which is being type-checked.

Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode.