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

Lawrence Paulson lp15 at cam.ac.uk
Mon Nov 3 13:12:13 CET 2014


I have to admit: although I distinctly remember the name pairself, I can’t imagine what I could have been thinking when I chose this name. Your suggestions make a lot more sense.

Larry

> On 3 Nov 2014, at 09:08, Makarius <makarius at sketis.net> wrote:
> 
> 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