1/1: Building CaseBlock (CaseBlock.idr)Main> Main.foo : (x : Nat) -> (case x of { 0 => Nat -> Nat ; S k => Nat })Main> Prelude.elem : Eq a => a -> List a -> Boolelem x [] = Falseelem x (y :: ys) = if x == y then True else elem x ysMain> PrimIO.io_bind : (1 act : IO a) -> (1 k : (a -> IO b)) -> IO bio_bind (MkIO fn) = \1 k => MkIO (\1 w => (case fn w of { MkIORes x' w' => case k x' of { MkIO res => res w' } }))Main> Bye for now!
1/1: Building CaseBlock (CaseBlock.idr)
Main> Main.foo : (x : Nat) -> (case x of { 0 => Nat -> Nat ; S k => Nat })
Main> Prelude.elem : Eq a => a -> List a -> Bool
elem x [] = False
elem x (y :: ys) = if x == y then True else elem x ys
Main> PrimIO.io_bind : (1 act : IO a) -> (1 k : (a -> IO b)) -> IO b
io_bind (MkIO fn) = \1 k => MkIO (\1 w => (case fn w of { MkIORes x' w' => case k x' of { MkIO res => res w' } }))
Main> Bye for now!