comparison lib/ur/option.ur @ 846:0d30e6338c65

Some standard library reorgs and additions; handle mutual datatypes better in Specialize
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Jun 2009 18:11:59 -0400
parents 74a1e3bdf430
children da3ec6014d2f
comparison
equal deleted inserted replaced
845:6725d73c3c31 846:0d30e6338c65
1 datatype t = datatype Basis.option 1 datatype t = datatype Basis.option
2
3 fun eq [a] (_ : eq a) =
4 mkEq (fn x y =>
5 case (x, y) of
6 (None, None) => True
7 | (Some x, Some y) => x = y
8 | _ => False)
2 9
3 fun isSome [a] x = 10 fun isSome [a] x =
4 case x of 11 case x of
5 None => False 12 None => False
6 | Some _ => True 13 | Some _ => True
7 14
8 fun mp [a] [b] f x = 15 fun mp [a] [b] f x =
9 case x of 16 case x of
10 None => None 17 None => None
11 | Some y => Some (f y) 18 | Some y => Some (f y)
19
20 fun bind [a] [b] f x =
21 case x of
22 None => None
23 | Some y => f y