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.

What to do with options following non-options.

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