[isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 30 20:07:23 CET 2014

>>> 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«?.

A further idea would be to have proper auxiliary definitions for ML
records also…



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141030/6059db76/attachment.sig>

More information about the isabelle-dev mailing list