Mercurial > urweb

annotate lib/ur/option.ur @ 1277:1e6a4f9d3e4a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More generous wildification, covering map-records
author Adam Chlipala <adamc@hcoop.net>
date Sun, 13 Jun 2010 10:55:20 -0400
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