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}?
Cheers,
René
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
