Enumerating all simply typed lambda terms of a given type 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?
This question has been considered several times in the academic community, from the practical:

Yakushev &amp; Jeuring, Enumerating Well-Typed Terms Generically

Fetsher &amp; al, Making Random Judgments: Automatically Generating
Well-Typed Terms from the Definition of a Type-System

to the more theoretical

Grygiel &amp; Lescanne, Counting and generating lambda terms

Implementations can pretty easily be found online. I didn't find any that addressed a system with iterators per se, but it shouldn't be a stretch from what already exists.