Generator function to monotonically return the "next" Natural?

I’m struggling conceptually to create an indexing function, the function should behave like the take-a-ticket paper sometimes found in public service offices, each call to nextNatural should yield a monotonically increasing number

I see that the prelude has List/generate, and Natural/enumerate.

I think I ran into a corner case, where it’s just outside the “totalness” of the language, and the general algebraic nature to have stateful generator functions?

Thanks in advance. The use-case, by the way is to enumerate nodes in my graph with “stable” ints according to the order in which they are produced, I could post-process my List Graph (which anyway gets folded into a List/fold Graph g Graph foldFn emptyGraph and maybe enumerate the nodes here in a stable way using something like a Natural/Enumerate as I fold the List Graph into a Graph?

Thanks in advance, loving the metal gymnastics I’m having to learn here, it’s really rewarding.

It’s hard to say without knowing more details, but if you want to do this efficiently then you’ll want to find some way to do this in terms of the List/indexed builtin:

List/indexed : ∀(a : Type) → List a → List { index : Natural, value : a }