gamarjoba.lean

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

random_game.lean

@@ -1,34 +0,0 @@
-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 ()