blob: 292d011ead60bd1ef0319fa12d433ee9cd4d1b88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Module Option.
Definition default {T : Type} (x : T) (u : option T) : T :=
match u with
| Some y => y
| _ => x
end.
Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T :=
match u with
| Some y => Some (f y)
| _ => None
end.
Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T :=
match a with
| Some x => map (f x) b
| _ => None
end.
End Option.
|
