Zulip Chat Archive

Stream: lean4

Topic: Infinite For Loop


Cole Shepherd (Dec 02 2022 at 03:42):

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 (Dec 02 2022 at 04:00):

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 (Dec 02 2022 at 04:42):

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


Last updated: Dec 20 2023 at 11:08 UTC