@@ -6,13 +6,26 @@ public export record Identity (a : Type) where
6 constructor Id
6 constructor Id
7 runIdentity : a
7 runIdentity : a
9−implementation Functor Identity where
9+Functor Identity where
10 map fn (Id a) = Id (fn a)
10 map fn (Id a) = Id (fn a)
12−implementation Applicative Identity where
12+Applicative Identity where
13 pure x = Id x
13 pure x = Id x
15 (Id f) <*> (Id g) = Id (f g)
14 (Id f) <*> (Id g) = Id (f g)
17−implementation Monad Identity where
16+Monad Identity where
18 (Id x) >>= k = k x
17 (Id x) >>= k = k x
19+Show a => Show (Identity a) where
20+ showPrec d (Id x) = showCon d "Id" $ showArg x
22+Eq a => Eq (Identity a) where
23+ (Id x) == (Id y) = x == y
25+Ord a => Ord (Identity a) where
26+ compare (Id x) (Id y) = compare x y
28+Enum a => Enum (Identity a) where
29+ toNat (Id x) = toNat x
30+ fromNat n = Id $ fromNat n
31+ pred (Id n) = Id $ pred n