Lean's function types describe more than just the function's domain and range. They also provide instructions for elaborating application sites by indicating that some parameters are to be discovered automatically via unification or type class synthesis, that others are optional with default values, and that yet others should be synthesized using a custom tactic script. Furthermore, their syntax contains support for abbreviating curried functions.
Dependent function types may include multiple parameters that have the same type in a single set of parentheses:
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
This is equivalent to repeating the type annotation for each parameter name in a nested function type.
Function types can describe functions that take implicit, instance implicit, optional, and automatic parameters. All but instance implicit parameters require one or more names.
term ::= ...
| Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
term ::= ... |(ident* : term := byExplicit binder, like `(x y : A)` or `(x y)`. Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.tacticSeq) → termA sequence of tactics in brackets, or a delimiter-free indented sequence of tactics. Delimiter-free indentation is determined by the *first* tactic of the sequence.
term ::= ...
| Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.
In `@` explicit mode, implicit binders behave like explicit binders.
term ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
term ::= ...
| Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
term ::= ...
| Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.