Next: Propositions and Universes
Up: Type Theory Preliminaries
Previous: Cartesian Products
If 
and 
are types, then 
denotes the type of
all computable (total) functions from to . The
canonical elements of this type are lambda terms, 
. If
we let 
denote the substitution of the term 
for
all free occurrences of 
in 
, then we require of
that 
for all terms denoting elements of . If 
and 
, then 
denotes the application
of 
to argument . We know that 
. See fun_1.
Recursive functions are defined in the style of ML. We use the form
to introduce a recursive definition, for example,
if 
then 1 else 
fi. This invokes an ML tactic called
add_rec_def with 
as arguments. The tactic adds an
abstraction named by the function name, e.g. fact. The abstraction is
based on a recursion combinator such as 
. For example, 
is the combinator added for factorial.
The abstraction is made invisible by various tactics that fold and
unfold instances of the definiton, so the user need not be aware of
the underlying 
-calculus foundations. In the automata
library we use a recursive function to define the analogue of
from HU. Informally, the definition is
The actual definition is
