agentultra/lean-for-hackers

Problems in the random number guessing game code

oxarbitrage opened this issue · 3 comments

oxarbitrage commented

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:

lean4hackers

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

fzyzcjy commented

Hi did you solve it? Thanks

fzyzcjy commented

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

  • 👍1
oxarbitrage commented

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

  • 😄1