On Sat, 27 Apr 2013, Florian Haftmann wrote:
fun gen_foo prep_1 … prep_n raw_x_1 … raw_x_n ctxt =
let
val x_1 = prep_1 ctxt raw_x_1;
…
val x_n = prep_n ctxt raw_x_n;
in
ctxt
| …
end;
val foo = gen_foo cert_1 … cert_n;
val foo_cmd = gen_foo read_1 … read_n;
Here,
Hey Florian.
Just my two cents, but does uncurrying buy you anything here?
The function doing the actual work, do_foo in your example, has not
been given a name and type before. So you're free to have it accept a tuple:
fun do_foo (x_1, x_2, ... x_n) = ...
And now val foo_cmd =
Hi all,
when Isabelle packages (in the widest sense) provide an interface to the
user, the following pattern is common practice:
fun gen_foo prep_1 … prep_n raw_x_1 … raw_x_n ctxt =
let
val x_1 = prep_1 ctxt raw_x_1;
…
val x_n = prep_n ctxt raw_x_n;
in
ctxt
| …
