Does Idris 2 have anything similar to Haskell's RecursiveDo. I have certain values that I would like to use before they are defined while in the IO monad. I am trying to build a cyclical FRP network. They implement the following interface:
interface Loop (a : Type) where
loop : (a -> IO (b, a)) -> IO b
However using loop is ugly. Is there a better way?