Let be two types. We introduce a type called the function type. The constructors for this type are written as
where and .
These can be computed (on application) using -reduction:
which says take and replace all occurrences of with .
Revision on October 11, 2018 at 12:50:29 by Ali Caglayan. See the history of this page for a list of all contributions to it.