-- This file:
--   http://anggtwu.net/LEAN/fpl_067.lean.html
--   http://anggtwu.net/LEAN/fpl_067.lean
--          (find-angg "LEAN/fpl_067.lean")
-- See: (find-fplean4page 67 "Hello, {name}!")
--      (find-fplean4text 67 "Hello, {name}!")
--      (find-es "lean" "let")
--
-- (defun e () (interactive) (find-angg "LEAN/fpl_067.lean"))
-- (find-es "rcirc" "header-line-format")
-- header-line-format
-- (find-efunctiondescr 'window-parameter)
-- (find-elnode "Index" "* window-parameter:")
-- lsp-headerline--string
-- (find-eppp (window-parameters))

def main : IO Unit := do
  let stdin  ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace

  stdout.putStrLn s!"Hello, {name}!"

#check IO
#check EIO

#check         (· == '!')
#check fun x => x == '!'
#eval ("Hello!!!").dropRightWhile (· == '!')
#eval "Hello... ".dropRightWhile (fun c => not (c.isAlphanum))


/-
| (find-elan4leanfile "Lean/")
| (find-lean4file "doc/")
| (find-lean4file "doc/tour.md")
| (find-angg ".emacs.papers" "fplean4")

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
lean --run fpl_067.lean
  Edr x

-/