# Implicit and explicit parameters

When declaring a type family or constant, the Twelf programmer often needs to use **universally quantified** parameters, and has the choice of making the parameter **implicit** or **explicit**. The article on converting between implicit and explicit parameters discusses how these two ways of doing things can be derived from each other.

Using fully **explicit parameters** means that all variables are *bound* by being placed within curly braces `{}`. The type family or constant generally has more arguments when using this form.

Using **implicit parameters** means that variables are not put within curly braces. Twelf assumes an identifier is meant to be a universally quantified parameter if the identifier starts with an uppercase letter *and* if that identifier has not been bound or defined anywhere else. This is essentially an interface aspect allowing for simpler code—internally, Twelf applies type reconstruction to identify the type of the universally quantified variables and converts the implicit parameters into explicit parameters.

The implicit parameters style is more concise and is often cleaner; however, in some cases it is necessary to use explicit parameters (for instance, a `%terminates` or `%total` declaration can refer to explicit parameters, not implicit parameters), and it may make stylistic sense in other situations as well.

Examples of the two different styles follow, using the language from the article on converting between implicit and explicit parameters which is omitted for brevity. The Twelf output is included - note that the Twelf output *always* writes out explicit parameters,^{[?]} even if the definition is using implicit parameters; therefore the two examples have almost exactly the same output from Twelf.

### Implicit parameters

translate-i : of M A -> of M' A -> type. %mode translate-i +D -D'.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)translate-i : {M:exp} {A:typ} {M':exp} of M A -> of M' A -> type. %mode +{M:exp} +{A:typ} -{M':exp} +{D:of M A} -{D':of M' A} (translate-i D D').

%% OK %%

### Explicit parameters

Note that in this example we use slightly bad style, capitalizing our bound variables `M`, `A`, and `M'`.

translate-e : {M : exp}{A : typ} {M' : exp} of M A -> of M' A -> type. %mode translate-e +M +A -M' +D -D'.

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)translate-e : {M:exp} {A:typ} {M':exp} of M A -> of M' A -> type. %mode +{M:exp} +{A:typ} -{M':exp} +{D:of M A} -{D':of M' A} (translate-e M A M' D D').

%% OK %%

## See also

- Full LF in the tutorial Proving metatheorems with Twelf discusses implicit and explicit parameters in the section "Twelf conveniences."