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. Of course, the type cannot be any type. It must be a type 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 section 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