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

Makarius makarius at sketis.net
Mon Nov 3 10:08:09 CET 2014


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


More information about the isabelle-dev mailing list