-- This file:
--   http://anggtwu.net/LEAN/fpl_071.lean.html
--   http://anggtwu.net/LEAN/fpl_071.lean
--          (find-angg "LEAN/fpl_071.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/fpl_071.lean"))
-- (defun o () (interactive) (find-angg "LEAN/fpl_067.lean"))
-- See: (find-fplean4page 71 "def twice (action : IO Unit) :")
--      (find-fplean4text 71 "def twice (action : IO Unit) :")
--      (find-fplean4page 72 "def nTimes (action : IO Unit) :")
--      (find-fplean4text 72 "def nTimes (action : IO Unit) :")
--      (find-es "lean" "let")

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

def nTimes (action : IO Unit) : Nat → IO Unit
  | 0 => pure ()
  | n + 1 => do
    action
    nTimes action n

def countdown : Nat → List (IO Unit)
  | 0 => [IO.println "Blast off!"]
  | n + 1 => IO.println s!"{n + 1}" :: countdown n

def from5 : List (IO Unit) := countdown 5

#check from5
#check from5.length
#eval from5.length

def runActions : List (IO Unit) → IO Unit
  | [] => pure ()
  | act :: actions => do
    act
    runActions actions

def main : IO Unit := runActions from5

def foo : Nat := 5
#eval foo




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