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

[Florian Haftmann]

>>> 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…

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>