Mercurial > urweb
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 |