Generator function to monotonically return the "next" Natural?

#1

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.

#2

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 }