Infinite For Loop

Stream: lean4

[Cole Shepherd]

How can I write an infinite loop with for syntax in a do block? I know there are other ways of accomplishing this (ex: partial function with infinite recursion), but I'm just curious how I'd accomplish this with a for loop. Can I create a lazy infinite list somehow and iterate through it? Would that be performant?

[Jason Rute]

If you modify the code for docs4#Std.Range.forIn you can make an infinite loop. Here is some code from the early days of Lean 4. I don’t know if it is still valid: https://gist.github.com/jasonrute/bb62203cb7debba0122ef69740ac078d

[Jason Rute]

Oh it looks like there is now docs4#Lean.Loop.forIn withwhile and repeat notation.