mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
9 lines
409 B
Plaintext
9 lines
409 B
Plaintext
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) = (x == y) || Delay (elem x ys)
|
|
Main> PrimIO.io_bind : (1 _ : IO a) -> (1 _ : (a -> IO b)) -> IO b
|
|
io_bind (MkIO fn) k = MkIO (\1 w => let MkIORes x' w' = fn w in let MkIO res = k x' in res w')
|
|
Main> Bye for now!
|