agentultra/lean-for-hackers

lean-for-hackers's Issues

running Lean from the command line

Instead of calling lean my_file.lean and having #eval main in your source file, I recommend you call Lean lean --run my_file.lean without the #eval statement. It will run your main function

Problems in the random number guessing game code

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 :)

More lean programming tutorial

Great work here! However, I struggle to find more lean 3 programming tutorials, including documentation of lean library. Where can I find these tutorials?

nat.to_string

this is not working anymore. I used repr.