On Thu, 30 Oct 2014, Florian Haftmann wrote:
Isabelle/ML has antiquotations as some kind of macro language. It can
do certain things better than the C preprocessor, although one always
needs to be careful to stay within reason.
How about this?
ap2 f (x, y) = (f x, f y)
@{ap n} f (x1, ..., xn) = (f x1, ..., f xn)
Maybe even this as well?
@{ap n(k)} f (x1, ..., xn) = (x1, ..., f xk, ..., xn)
That might be occasionally useful to map field 1, or 2, or 3 of a triple:
@{ap 3(1)}, @{ap 3(2)}, @{ap 3(3)}. The existing combinators apfst,
apsnd fit into the same scheme.
Both have there uses. I am not sure whether »ap« is the right name.
»apfst« and »apsnd« are of course old-standing items, but when something
new enters the stage further thoughts should be spent. Must confess I
have no better proposal at hand. Or maybe »apply«?.
Larry, you have introduced the "pairself" name some decades ago. How do
you feel about it being called "ap2" or "apply2"?
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org 777,356 people so far
----------------------------------------------------------------------------_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
