type bool = True | False type ('a) option = Some of 'a | None let is_some = fun ['a] (x : 'a option) => match x with | Some(_) => True | None => False end let forall 'a ornament is_some ['a] : 'a option -> bool type key = Key let rec compare : key -> key -> int = compare type set = Empty | Node of key * set * set let empty = Empty let rec find : key -> set -> bool = fun (k : key) (s : set) => match s with | Empty => False | Node(k',l,r) => match eq (compare k k') 0 with | True => True | False => match gt (compare k k') 0 with | True => find k l | False => find k r end end end type ('a) map = MEmpty | MNode of key * 'a * 'a map * 'a map let rec keys : forall 'a. 'a map -> set = fun ['a] (m : 'a map) => match m with | MEmpty => Empty | MNode(k,_,l,r) => Node(k,keys ['a] l,keys ['a] r) end let forall 'a ornament keys ['a] : 'a map -> set let rec mempty : forall 'a. 'a map = fun ['a] => MEmpty['a] let rec mfind : forall 'a. key -> 'a map -> 'a option = fun ['a] (k0 : key) (s : 'a map) => match s with | MEmpty => None['a] | MNode(k1,_,l,r) => match eq (compare k0 k1) 0 with | True => Some['a](??y__25__27??) | False => match gt (compare k0 k1) 0 with | True => mfind [???] k0 l | False => mfind [???] k0 r end end end