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 quadruple
> Both Isabelle/ML and Isabelle/Scala have become quite able system
> programming languages in recent years, so the need for funny scripting
> languages is more and more diminished.
I think so, too. Borderline cases could be scenarios where an
established standard technology is necessary for whic
In 3094b0edd6b5 I needed to change a document comment {* ..*} to a
source comment (* .. *). Looks like using the @{ML ..} antiquotation in
a document comment does not work. Latex does not allow \verb inside
commands-parameters.
Is it possible to change \verb to \texttt, with the necessary _ -> \_
