Agda.Syntax.Concrete.Attribute

An attribute is a modifier for ArgInfo.

Parsed attribute.

(Conjunctive constraint.)

Modifiers for Relevance.

Modifiers for Quantity.

Information about attributes (attribute, range, printed representation).

This information is returned by the parser. Code that calls the parser should, if appropriate, complain if support for the given attributes has not been enabled. This can be taken care of by checkAttributes, which should not be called until after pragma options have been set.

Modifiers for Polarity.

Modifiers for Quantity.

Concrete syntax for all attributes.

Parsing a string into an attribute.

Parsing an expression into an attribute.

Setting an attribute (in e.g. an Arg). Overwrites previous value.

Setting some attributes in left-to-right order. Blindly overwrites previous settings.

Setting Relevance if unset.

Setting Quantity if unset.

Setting Cohesion if unset.

Setting ModalPolarity if unset.

Setting Lock if unset.

Setting an unset attribute (to e.g. an Arg).

Setting a list of unset attributes.