More random Lean stuff I guess

Changes

1 changed files (+17/-0)

• IO.lean (new)
  • @@ -0,0 +1,17 @@
    + def main : IO Unit := do + -- Read input immediately without waiting for newline + _ ← IO.Process.run { + cmd := "stty" + args := #["-F", "/dev/tty", "cbreak", "min", "1"], + } + -- Hide user input + _ ← IO.Process.run { + cmd := "stty" + args := #["-F", "/dev/tty", "-echo"], + } + let stdin ← IO.getStdin + while true do + let a ← stdin.read 1 + match String.fromUTF8? a with + | some str => IO.println s!"Hello {str}" + | none => return