mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-28 14:06:26 +03:00
7aa8a71f8f
Need to add by full name, due to ordering of loading (the name it's attached to may not be resolved yet!). This doesn't seem to cause any performance problems but we can revisit if it does.
45 lines
768 B
Idris
45 lines
768 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)
|