Compare commits
2 Commits
7912636be6
...
be618f9a74
Author | SHA1 | Date | |
---|---|---|---|
|
be618f9a74 | ||
|
1a5d5f7b59 |
@ -2,6 +2,7 @@ import system.io
|
|||||||
|
|
||||||
open io
|
open io
|
||||||
|
|
||||||
|
#check (++)
|
||||||
def greet (s : string) : io unit :=
|
def greet (s : string) : io unit :=
|
||||||
put_str $ "Hello, " ++ s ++ "!\n"
|
put_str $ "Hello, " ++ s ++ "!\n"
|
||||||
|
|
||||||
|
34
random_game.lean
Normal file
34
random_game.lean
Normal file
@ -0,0 +1,34 @@
|
|||||||
|
import system.io
|
||||||
|
|
||||||
|
open char
|
||||||
|
open list
|
||||||
|
open io
|
||||||
|
|
||||||
|
|
||||||
|
def rand_range(lo : nat)(hi: nat) : io nat := do
|
||||||
|
r <- io.cmd { cmd := "head", args := ["-c 80", "/dev/urandom"] },
|
||||||
|
let seed := foldl (+) 0 $ map to_nat r.to_list,
|
||||||
|
let gen := mk_std_gen seed,
|
||||||
|
let (target, _) := rand_nat gen lo hi,
|
||||||
|
return target
|
||||||
|
|
||||||
|
def get_guess : io nat := do
|
||||||
|
put_str "Guess a number between 1 and 100 (inclusive)\n",
|
||||||
|
put_str "Your guess: ",
|
||||||
|
response <- get_line,
|
||||||
|
return $ string.to_nat response
|
||||||
|
|
||||||
|
def main : io unit := do
|
||||||
|
target <- rand_range 1 100,
|
||||||
|
iterate 20 $ λ i,
|
||||||
|
if i > 0 then do {
|
||||||
|
put_str $ "You have " ++ (to_string i) ++ " guesses left\n",
|
||||||
|
guess <- get_guess,
|
||||||
|
match cmp guess target with
|
||||||
|
| ordering.eq := do { put_str "\nYou win!\n", return none }
|
||||||
|
| ordering.gt := do { put_str "\ntoo high\n", return $ some (i - 1) }
|
||||||
|
| ordering.lt := do { put_str "\ntoo low\n", return $ some (i - 1) }
|
||||||
|
end
|
||||||
|
} else
|
||||||
|
return none,
|
||||||
|
return ()
|
Loading…
Reference in New Issue
Block a user