mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 02:31:50 +03:00
a972778eab
They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
45 lines
766 B
Idris
45 lines
766 B
Idris
mutual
|
|
data MyBool = MyFalse | MyTrue
|
|
|
|
even : Nat -> MyBool
|
|
even (S k) = odd k
|
|
even Z = MyTrue
|
|
|
|
odd : Nat -> MyBool
|
|
odd (S k) = even k
|
|
odd Z = MyFalse
|
|
|
|
eodd : Nat -> (Bool, Bool)
|
|
eodd num = (isEven num, isOdd num)
|
|
where
|
|
mutual
|
|
isEven : Nat -> Bool
|
|
isEven (S k) = isOdd k
|
|
isEven Z = True
|
|
|
|
isOdd : Nat -> Bool
|
|
isOdd (S k) = isEven k
|
|
isOdd Z = False
|
|
|
|
data Box : Type -> Type where
|
|
MkBox : a -> Box a
|
|
|
|
mutual
|
|
Functor Box where
|
|
map f b
|
|
= do b' <- b
|
|
pure (f b')
|
|
|
|
Applicative Box where
|
|
(<*>) f a
|
|
= do f' <- f
|
|
a' <- a
|
|
pure (f' a')
|
|
pure = MkBox
|
|
|
|
Monad Box where
|
|
(>>=) (MkBox val) k = k val
|
|
|
|
boxy : Box Integer
|
|
boxy = map (*2) (MkBox 20)
|