Micah (1) [Avatar] Offline
#1
Hi,

In Section 11.2.2, Executing Infinite Processes, run is defined as follows:

data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

run : InfIO -> IO ()
run (Do action cont) = do res <- action
                          run (cont res)


The book says that this function is not total, but when I check it in the repl it says that it is total.

Which is correct?

Thanks,
Micah