>>> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
