comparison lib/ur/option.ur @ 944:da3ec6014d2f

Filters implementation type-checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 15:48:53 -0400
parents 0d30e6338c65
children 8c37699de273
comparison
equal deleted inserted replaced
943:e2194a6793ae 944:da3ec6014d2f
4 mkEq (fn x y => 4 mkEq (fn x y =>
5 case (x, y) of 5 case (x, y) of
6 (None, None) => True 6 (None, None) => True
7 | (Some x, Some y) => x = y 7 | (Some x, Some y) => x = y
8 | _ => False) 8 | _ => False)
9
10 fun isNone [a] x =
11 case x of
12 None => True
13 | Some _ => False
9 14
10 fun isSome [a] x = 15 fun isSome [a] x =
11 case x of 16 case x of
12 None => False 17 None => False
13 | Some _ => True 18 | Some _ => True