app package:Agda
Ordinary (binary) application.
ex: e e, e {e}, or e {x = e}
Gather applications to expose head and spine.
Note: everything is an application, possibly of itself to 0 arguments
Compose with cohesion flag from the left. This function is e.g. used
to update the cohesion information on pattern variables a
after a match against something of cohesion rel.
Compose with modality flag from the left. This function is e.g. used
to update the modality information on pattern variables a
after a match against something of modality q.
Compose with polarity flag from the left. This function is e.g. used
to update the polarity information on pattern variables a
after a match against something of polarity pol.
Compose with quantity flag from the left. This function is e.g. used
to update the quantity information on pattern variables a
after a match against something of quantity q.
Compose with relevance flag from the left. This function is e.g. used
to update the relevance information on pattern variables a
after a match against something rel.
Does a function application need brackets?
Does a function application need brackets?
Do we prefer a lambda argument with or without parens?
Apply an attribute to thing (usually
Arg). This will fail if
one of the attributes is already set in the thing to something else
than the default value.
Apply some attributes to some binders.
Apply attributes to thing (usually
Arg). Expects a reversed
list of attributes. This will fail if one of the attributes is already
set in the thing to something else than the default value.