Ur/Web: lib/ur/option.ur annotate

Filters implementation type-checking

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 15 Sep 2009 15:48:53 -0400
parents	0d30e6338c65
children	8c37699de273

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@944	10 fun isNone [a] x =
adamc@944	11 case x of
adamc@944	12 None => True
adamc@944	13 \| Some _ => False
adamc@944	14
adamc@841	15 fun isSome [a] x =
adamc@841	16 case x of
adamc@841	17 None => False
adamc@841	18 \| Some _ => True
adamc@844	19
adamc@844	20 fun mp [a] [b] f x =
adamc@844	21 case x of
adamc@844	22 None => None
adamc@844	23 \| Some y => Some (f y)
adamc@846	24
adamc@846	25 fun bind [a] [b] f x =
adamc@846	26 case x of
adamc@846	27 None => None
adamc@846	28 \| Some y => f y

Mercurial > urweb