Problems in the random number guessing game code

[oxarbitrage]

Hey there, i was checking this guide mainly trying to figure out how the iterate works in the system monad. However, it seems that this specific part of the code is having some problems in recent versions of lean 3:

I will send a fix if i eventually figure it out, any help is welcome in the meantime :)

[fzyzcjy]

Hi did you solve it? Thanks

[fzyzcjy]

I guess it is the "1" that should be removed?

[oxarbitrage]

Thanks @fzyzcjy , that was pretty easy to fix, i should had tried harder. I pushed a fix #6