Mercurial > urweb
annotate lib/ur/option.ur @ 1148:a48966743c37
AM_INIT_AUTOMAKE with no-define (to fix some NetBSD and OS X problems)
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 06 Feb 2010 13:27:05 -0500 |
parents | 757dbac0454d |
children | a99b743a3087 |
rev | line source |
---|---|
adamc@841 | 1 datatype t = datatype Basis.option |
adamc@841 | 2 |
adamc@846 | 3 fun eq [a] (_ : eq a) = |
adamc@846 | 4 mkEq (fn x y => |
adamc@846 | 5 case (x, y) of |
adamc@846 | 6 (None, None) => True |
adamc@846 | 7 | (Some x, Some y) => x = y |
adamc@846 | 8 | _ => False) |
adamc@846 | 9 |
adamc@961 | 10 fun ord [a] (_ : ord a) = |
adamc@961 | 11 mkOrd {Lt = fn x y => |
adamc@961 | 12 case (x, y) of |
adamc@961 | 13 (None, Some _) => True |
adamc@961 | 14 | (Some x, Some y) => x < y |
adamc@961 | 15 | _ => False, |
adamc@961 | 16 Le = fn x y => |
adamc@961 | 17 case (x, y) of |
adamc@961 | 18 (None, _) => True |
adamc@961 | 19 | (Some x, Some y) => x <= y |
adamc@961 | 20 | _ => False} |
adamc@961 | 21 |
adamc@944 | 22 fun isNone [a] x = |
adamc@944 | 23 case x of |
adamc@944 | 24 None => True |
adamc@944 | 25 | Some _ => False |
adamc@944 | 26 |
adamc@841 | 27 fun isSome [a] x = |
adamc@841 | 28 case x of |
adamc@841 | 29 None => False |
adamc@841 | 30 | Some _ => True |
adamc@844 | 31 |
adamc@844 | 32 fun mp [a] [b] f x = |
adamc@844 | 33 case x of |
adamc@844 | 34 None => None |
adamc@844 | 35 | Some y => Some (f y) |
adamc@846 | 36 |
adamc@846 | 37 fun bind [a] [b] f x = |
adamc@846 | 38 case x of |
adamc@846 | 39 None => None |
adamc@846 | 40 | Some y => f y |
adamc@1068 | 41 |
adamc@1068 | 42 fun get [a] (x : a) (o : option a) = |
adamc@1068 | 43 case o of |
adamc@1068 | 44 None => x |
adamc@1068 | 45 | Some v => v |