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

René Thiemann rene.thiemann at uibk.ac.at
Fri Oct 24 08:07:27 CEST 2014

Dear all,

> How about this?
>  ap2 f (x, y) = (f x, f y)
>  @{ap n} f (x1, ..., xn) = (f x1, ..., f xn)

@{ap n} sounds reasonable to me, however, due to the presence of apfst and apsnd one might
think about adding an "all" to indicate that the function is applied to all element. So what about
@{ap_all n}?


More information about the isabelle-dev mailing list