Compare commits

...

2 Commits

Author SHA1 Message Date
Greg Shuflin be618f9a74 Add random game 2022-05-30 19:22:44 -07:00
Greg Shuflin 1a5d5f7b59 Check directive 2022-05-30 19:03:42 -07:00
2 changed files with 35 additions and 0 deletions

View File

@ -2,6 +2,7 @@ import system.io
open io
#check (++)
def greet (s : string) : io unit :=
put_str $ "Hello, " ++ s ++ "!\n"

34
random_game.lean Normal file
View 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 ()