equal
deleted
inserted
replaced
4 General-purpose functions used by the Sledgehammer modules. |
4 General-purpose functions used by the Sledgehammer modules. |
5 *) |
5 *) |
6 |
6 |
7 signature SLEDGEHAMMER_UTIL = |
7 signature SLEDGEHAMMER_UTIL = |
8 sig |
8 sig |
9 val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c |
|
10 val plural_s : int -> string |
9 val plural_s : int -> string |
11 val serial_commas : string -> string list -> string list |
10 val serial_commas : string -> string list -> string list |
12 val replace_all : string -> string -> string -> string |
11 val replace_all : string -> string -> string -> string |
13 val remove_all : string -> string -> string |
12 val remove_all : string -> string -> string |
14 val timestamp : unit -> string |
13 val timestamp : unit -> string |
21 val specialize_type : theory -> (string * typ) -> term -> term |
20 val specialize_type : theory -> (string * typ) -> term -> term |
22 end; |
21 end; |
23 |
22 |
24 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
23 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = |
25 struct |
24 struct |
26 |
|
27 fun pairf f g x = (f x, g x) |
|
28 |
25 |
29 fun plural_s n = if n = 1 then "" else "s" |
26 fun plural_s n = if n = 1 then "" else "s" |
30 |
27 |
31 fun serial_commas _ [] = ["??"] |
28 fun serial_commas _ [] = ["??"] |
32 | serial_commas _ [s] = [s] |
29 | serial_commas _ [s] = [s] |