General recursion in type theory

The old way

• Any total, generally recursive function can be represented in type theory by using the accessibility predicate, provided you have a size measure that decreases in the recursive calls. [Acz77,Nor88]
• The method can be cumbersome, since termination proofs becomes intertwined with the function definition.