Arg package:Agda

Named argument, like x in {x = v}

Describes whether an option takes an argument or not, and if so how the argument is injected into a value of type a.

A function argument can be hidden and/or irrelevant.

Names in binders and arguments.

Type of argument lists.

Usage status of function arguments in treeless code.

Call matrix indices = function argument indices. Machine integer Int is sufficient, since we cannot index more arguments than we have addresses on our machine.

Type of the argument.

Sometimes we want a different kind of binder/pi-type, without it supporting any of the Modality interface.