2.3 Forced type
In some cases, one want to assign a particular type to a term. The
syntax to force the type of a term is the following:
| term |
::= |
( term :: term ) |
It forces the first term to be of type the second term. The
type must be compatible with
the term. More precisely it must be either a type convertible to
the automatically inferred type (see chapter 4) or a type
coercible to it, (see 2.7). When the type of a
whole expression is forced, it is usually not necessary to give the types of
the variables involved in the term.
Example:
Coq < Definition ID := (X:Set) X -> X.
ID is defined
Coq < Definition id := (([X][x]x) :: ID).
id is defined
Coq < Check id.
id
: ID