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