search

leanprover-community / lean4-samples

Code samples for Lean 4
Apache License 2.0
67 stars 22 forks source link

Add a new Guess-my-number example. #2

Closed casavaca closed 2 years ago

leodemoura commented 2 years ago

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

lovettchris commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

@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 commented 2 years ago

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 commented 2 years ago

@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