General recursion in type theory

The new way

• Each generally recursive function is translated into two parts:
  1. A special purpose accessibility predicate, or domain predicate. It is inductively defined, based on the structure of the original function.
  2. A translated function that instead of general recursion on the original domain uses only structural recursion over the proof that the argument satisfies the domain predicate.