foo.idr

--loop, I don't even use pffft
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  Just g <- pure (stringToNat line) | Nothing => (printLn "Invalid String" *> guess target)
  let pffft = stringToNat line
  let g = case stringToNat line of
            Just p => p
            Nothing => 0
  case compare g target of
       EQ => do
         printLn "Richtig!"
       LT => do
         printLn "Mehr!"
         guess target
       GT => do
         printLn "Weniger"
         guess target

---

--no loop, there is no pffft but I do shadow the g
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  Just g <- pure (stringToNat line) | Nothing => (printLn "Invalid String" *> guess target)
  let g = case stringToNat line of
            Just p => p
            Nothing => 0
  case compare g target of
       EQ => do
         printLn "Richtig!"
       LT => do
         printLn "Mehr!"
         guess target
       GT => do
         printLn "Weniger"
         guess target

---

--loop, I don't shadow the g
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  let g = case stringToNat line of
            Just p => p
            Nothing => 0
  case compare g target of
       EQ => do
         printLn "Richtig!"
       LT => do
         printLn "Mehr!"
         guess target
       GT => do
         printLn "Weniger"
         guess target

---

-- no loop, I don't have the let at all
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  Just g <- pure (stringToNat line) | Nothing => (printLn "Invalid String" *> guess target)
  case compare g target of
       EQ => do
         printLn "Richtig!"
       LT => do
         printLn "Mehr!"
         guess target
       GT => do
         printLn "Weniger"
         guess target
         

--no loop, this is clearly a let/case bug
guess : (target : Nat) -> IO ()
guess target = do
  printLn "Rate die Zahl"
  line <- getLine
  let g = maybe 0 id (stringToNat line)
  case compare g target of
       EQ => do
         printLn "Richtig!"
       LT => do
         printLn "Mehr!"
         guess target
       GT => do
         printLn "Weniger"
         guess target