-- This file:
--   http://anggtwu.net/LEAN/ioprocess1.lean.html
--   http://anggtwu.net/LEAN/ioprocess1.lean
--          (find-angg "LEAN/ioprocess1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- Superseded by:
--   (find-angg "LEAN/luatree1.lean")
--
-- (defun e () (interactive) (find-angg "LEAN/ioprocess1.lean"))
-- (find-angg "LEAN/luatree.lean")
-- (find-fplean4page 71 "def twice (action : IO Unit) : IO Unit")
-- (find-fplean4text 71 "def twice (action : IO Unit) : IO Unit")
-- (find-fplean4page 79 "Worked Example: cat")
-- (find-fplean4text 79 "Worked Example: cat")
-- (find-fplean4page 164 "The Monad Type Class")
-- (find-fplean4text 164 "The Monad Type Class")
-- (find-fplean4page 165 "General Monad Operations")
-- (find-fplean4text 165 "General Monad Operations")




import Lean.Log
import Lean.Parser.Command
import Lean.DeclarationRange
import Lean.Data.Lsp.Utf16

#check List.mapM

-- (find-lean4prefile "Lean/Parser/Command.lean")

def twice (action : IO Unit) : IO Unit := do
  action
  action

def twice42 (action : IO Unit) : IO String := do
  action
  action
  return "42"


-- (find-lean4prefile "lake/Lake/Config/InstallPath.lean" "let out ← IO.Process.output {")
#check IO.Process.output
#print IO.Process.output
def pro1 := IO.Process.output { cmd := "echo", args := #["foo", "bar"] }
#check pro1
#print pro1
-- #eval pro1

#check  ["foo", "bar"]
#check #["foo", "bar"]

#eval let a := 2; a * a

#check pure 42
#check do return 42


def maain : IO Nat := do
  IO.println "hello"
  IO.println "world"
  return 0



def fooo : IO Nat := do
  let a ← pure 2
  let b ← pure 2
  return a * b

-- IO.println "Hello"

def foo : IO String := do
  let out ← IO.Process.output { cmd := "echo", args := #["foo", "bar"] }
  -- let exitcode := out.exitCode
  return out.stdout

#eval foo

/-

  let act : IO _ := do
    let out ← IO.Process.output {
      cmd := lean,
      args := #["--print-prefix"]
    }
    if out.exitCode == 0 then
      pure <| some <| FilePath.mk <| out.stdout.trim
    else
      pure <| none
  act.catchExceptions fun _ => pure none

-/






-- Local Variables:
-- coding:  utf-8-unix
-- End: