Intriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function: https://us.metamath.org/mpeuni/df-rdg.

Intriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function: https://us.metamath.org/mpeuni/df-rdg.html https://us.metamath.org/mpeuni/df-rdg.html Essentially, it's just doing a lazy fixpoint a la Haskell's fix function. The definition is a little more general, though, to make it work for both transfinite and well-founded recursions as well. This chashed out nicely in a sequence builder: https://us.metamath.org/mpeuni/df-seq.html https://us.metamath.org/mpeuni/df-seq.html which specializes to "normal" recursion.