From f6cfaea8a7eb777dae12337178c3b9a268459995 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 9 Jun 2009 18:11:59 -0400 Subject: Some standard library reorgs and additions; handle mutual datatypes better in Specialize --- lib/ur/option.ur | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'lib/ur/option.ur') diff --git a/lib/ur/option.ur b/lib/ur/option.ur index 5ec093c0..1f044002 100644 --- a/lib/ur/option.ur +++ b/lib/ur/option.ur @@ -1,5 +1,12 @@ datatype t = datatype Basis.option +fun eq [a] (_ : eq a) = + mkEq (fn x y => + case (x, y) of + (None, None) => True + | (Some x, Some y) => x = y + | _ => False) + fun isSome [a] x = case x of None => False @@ -9,3 +16,8 @@ fun mp [a] [b] f x = case x of None => None | Some y => Some (f y) + +fun bind [a] [b] f x = + case x of + None => None + | Some y => f y -- cgit v1.2.3