equal
deleted
inserted
replaced
6 |
6 |
7 signature SLEDGEHAMMER_UTIL = |
7 signature SLEDGEHAMMER_UTIL = |
8 sig |
8 sig |
9 val sledgehammerN : string |
9 val sledgehammerN : string |
10 val log2 : real -> real |
10 val log2 : real -> real |
11 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
|
12 val app_hd : ('a -> 'a) -> 'a list -> 'a list |
11 val app_hd : ('a -> 'a) -> 'a list -> 'a list |
13 val plural_s : int -> string |
12 val plural_s : int -> string |
14 val serial_commas : string -> string list -> string list |
13 val serial_commas : string -> string list -> string list |
15 val simplify_spaces : string -> string |
14 val simplify_spaces : string -> string |
16 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
15 val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b |
36 |
35 |
37 val sledgehammerN = "sledgehammer" |
36 val sledgehammerN = "sledgehammer" |
38 |
37 |
39 val log10_2 = Math.log10 2.0 |
38 val log10_2 = Math.log10 2.0 |
40 fun log2 n = Math.log10 n / log10_2 |
39 fun log2 n = Math.log10 n / log10_2 |
41 |
|
42 fun map3 xs = Ctr_Sugar_Util.map3 xs |
|
43 |
40 |
44 fun app_hd f (x :: xs) = f x :: xs |
41 fun app_hd f (x :: xs) = f x :: xs |
45 |
42 |
46 fun plural_s n = if n = 1 then "" else "s" |
43 fun plural_s n = if n = 1 then "" else "s" |
47 |
44 |