Add a new Guess-my-number example.

[casavaca]

No description provided.

[lovettchris]

Awesome thanks, I would love some word smithing which I can do or if you want to do them let me know and I'll complete the review here. I'm also thinking it would be great if there was a while loop until the user guesses the right answer. Also since you are using a do block, can the match Ord.compare become an if/then/else?

[leodemoura]

Thanks for submitting the PR. I have only a few minor comments.

[lovettchris]

@leodemoura, I will merge this PR so that I can work on the changes proposed by you and Sebastian and do some word smithing. I think Casavanca got busy with other stuff...

[leodemoura]

@leodemoura, I will merge this PR so that I can work on the changes proposed by you and Sebastian and do some word smithing. I think Casavanca got busy with other stuff...

Sure.

BTW, I just pushed the change @Kha suggested above for the Lean 4 repo.

[Kha]

@lovettchris FYI, since you have push access you should be able to push changes directly to the PR branch without merging it. Not that it matters much in this case of course since this repo is not exactly high-traffic.

[lovettchris]

@lovettchris FYI, since you have push access you should be able to push changes directly to the PR branch without merging it. Not that it matters much in this case of course since this repo is not exactly high-traffic.

really, does that work with forks? the code lives here: https://github.com/casavaca/lean4-samples

[lovettchris]

This is now pushed and fully edited, see https://github.com/leanprover/lean4-samples/tree/main/GuessMyNumber

And I enabled CI test runs which all pass:
https://github.com/leanprover/lean4-samples/actions/runs/2573009151

[leodemoura]

@lovettchris The following workaround with seeds is not needed anymore. I fixed this issue in the commit I linked above.

-- Generate a "random" number in [0, 99]
-- It's not actually random. We'll talk about it later.
def getSecret : IO Nat :=
  let seed ← (UInt64.toNat ∘ ByteArray.toUInt64LE!) <$> IO.getRandomBytes 8
  IO.setRandSeed seed
  IO.rand 0 99

The simpler version should be enough now:

-- Generate a "random" number in [0, 99]
def getSecret : IO Nat :=
  IO.rand 0 99