equal
deleted
inserted
replaced
3 Author: Alexander Krauss, TU Muenchen |
3 Author: Alexander Krauss, TU Muenchen |
4 |
4 |
5 A package for general recursive function definitions. |
5 A package for general recursive function definitions. |
6 Some fairly general functions that should probably go somewhere else... |
6 Some fairly general functions that should probably go somewhere else... |
7 *) |
7 *) |
8 |
|
9 |
|
10 |
8 |
11 structure FundefLib = struct |
9 structure FundefLib = struct |
12 |
10 |
13 fun map_option f NONE = NONE |
11 fun map_option f NONE = NONE |
14 | map_option f (SOME x) = SOME (f x); |
12 | map_option f (SOME x) = SOME (f x); |
17 | fold_option f (SOME x) y = f x y; |
15 | fold_option f (SOME x) y = f x y; |
18 |
16 |
19 fun fold_map_option f NONE y = (NONE, y) |
17 fun fold_map_option f NONE y = (NONE, y) |
20 | fold_map_option f (SOME x) y = apfst SOME (f x y); |
18 | fold_map_option f (SOME x) y = apfst SOME (f x y); |
21 |
19 |
22 (* ??? *) |
20 (* Ex: "The variable" ^ plural " is" "s are" vs *) |
23 fun eq_str (s : string, t) = (s = t) (* monomorphic equality on strings *) |
21 fun plural sg pl [x] = sg |
|
22 | plural sg pl _ = pl |
24 |
23 |
25 (* ==> logic.ML? *) |
24 (* ==> logic.ML? *) |
26 fun mk_forall v t = all (fastype_of v) $ lambda v t |
25 fun mk_forall v t = all (fastype_of v) $ lambda v t |
27 |
26 |
28 (* lambda-abstracts over an arbitrarily nested tuple |
27 (* lambda-abstracts over an arbitrarily nested tuple |