Other examples of inductive-recursive definitions include an informal definition of computability predicates used by Martin-Löf in an early normalization proof of intuitionistic type theory (Martin-Löf 1998 [1972]). There are also many natural examples of “small” inductive-recursive definitions, where the recursively defined (decoding) function returns an element of a type rather than a type.