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

Fix MonoReduce unsoundness with lets and fns

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 13 Jun 2009 15:42:24 -0400
parents	0d30e6338c65
children	da3ec6014d2f

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

Mercurial > urweb