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

[Dmitriy Traytel]

Antiquotations---bringing dependent types into Isabelle/ML :-)

This is really nice, Makarius. Thanks!

Dmitriy

On 08.10.2014 20:46, Makarius wrote:
> *** ML ***
>
> * Basic combinators map, fold, fold_map, split_list are available as
> parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
>
> This refers to Isabelle/9f10d82e8188.
>
>
> After seeing another split_list42 combinator, I could not resist to 
> make a fully general solution once and for all.  The changset also 
> eliminates some clones that have accumulated over the years.
>
> 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.
>
>
>     Makarius
>
> ---------------------------------------------------------------------------- 
>
>                               http://stop-ttip.org
> ---------------------------------------------------------------------------- 
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>