How can I enumerate all simply typed lambda terms which have a specified type?
More precisely, suppose we have the simply typed lambda calculus augmented with numerals and iteration, as described in this answer. How can I enumerate all lambda terms of type N (natural number)?
For example, the first few lambda terms of type N are
zero succ zero succ (succ zero), K zero zero succ (succ (succ zero)), K zero (suc zero), K (suc zero) zero, iter zero suc zero
and so on. How can I systematically continue this pattern, while ensuring that only well-typed terms are generated?