diff lib/ur/option.urs @ 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
line wrap: on
line diff
--- a/lib/ur/option.urs	Tue Jun 09 11:12:34 2009 -0400
+++ b/lib/ur/option.urs	Tue Jun 09 18:11:59 2009 -0400
@@ -1,5 +1,8 @@
 datatype t = datatype Basis.option
 
+val eq : a ::: Type -> eq a -> eq (t a)
+
 val isSome : a ::: Type -> t a -> bool
 
 val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b
+val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b