3.5. Implicit Arguments

A function type in fully elaborated form has the structure:

all <telescope>: <simple type>

all (x₁: A₁) (x₂: A₂) ... : R

Variables which do occur in the subsequent types or in the result type are potentially implicit arguments.

A potentially implicit argument can be made implicit by using braces instead of parentheses. I.e. in

all {x₁: A₁} ... : R

all {x₁} ... : R

the argument x₁ is declared as an implicit argument.

Many potentially implicit arguments are mandatory implicit. A potentially implicit argument x: A is mandatory implicit in the following cases:

• A in head normal form is a kind i.e. it is a sort or all <telescope>: Sort.

• The function type in which x: A occurs is a proposition.

Only in the case that the function type is not a proposition and A is not a kind, then the user can choose to make a potentially implicit argument implicit or not.

Rule:

Mandatory implicit arguments have to be declared within braces.