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