Operations.lidr 415 Bytes
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
> module Fun.Operations


> %default total
> %access public export
> %auto_implicits on


> |||
> pair : (a -> b, a -> c) -> a -> (b, c)
> pair (f, g) x = (f x, g x)


> |||
> cross : (a -> c) -> (b -> d) -> (a, b) -> (c, d)
> cross f g (x, y) = (f x, g y)


> |||
> modifyFun : {a : Type} -> {b : Type} -> (Eq a) =>
>             (a -> b) -> a -> b -> (a -> b)
> modifyFun f a b a' = if a' == a then b else f a'