Very nice job!
Amine.
PS: In Reflected Ferrack you start combutation with True, i.e. @{code
T}, if the input is @{term False}. Fortunately this does not happen
often.... Even with @{code} we still need to be careful...
Florian Haftmann wrote:
> New ML antiquotation 'code': takes constant as argument, generates
> corresponding code in background and inserts name of the corresponding
> resulting ML value/function/datatype constructor binding in place. All
> occurences of 'code' with a single ML block are generated simultaneously.
> Provides a generic and safe interface for instrumentalizing code
> generation. See HOL/ex/Code_Antiq for a toy example, or
> HOL/Complex/ex/ReflectedFerrack for a more ambitious application. In
> future you ought refrain from ad-hoc compiling generated SML code on
> the ML toplevel.
> Note that (for technical reasons) 'code' cannot refer to constants for
> which user-defined serializations are set. Refer to the corresponding
> ML counterpart directly in that cases.
>
> Florian
>
>
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
