Lines Matching refs:Error
15 exception Error = mlibUseful.Error;
81 val () = if l + 1 + r = size then () else raise Error "wrong size"
96 | EQUAL => raise Error "duplicate keys"
97 | GREATER => raise Error "unsorted"
111 | EQUAL => raise Error "left child has equal key"
112 | GREATER => raise Error "left child has greater priority"
119 | EQUAL => raise Error "right child has equal key"
120 | GREATER => raise Error "right child has greater priority"
134 handle Error err => raise Bug err)
313 fun treeDelete _ E _ = raise Error "RandomMap.delete: element not found"
453 fun treeNth E _ = raise Error "RandomMap.nth"
506 NONE => raise Error "RandomMap.get: element not found"