Re: [isabelle] value (code) doesn't complain when no code equations exist

To make it clear: ( ) denotes a print mode:

value [nbe] (iff) "(P::bool) â Q"
value [nbe] ("iff, xsymbols") "(P::bool) â Q"
value [nbe] "(P::bool) â Q"

Am 03.06.2015 um 11:42 schrieb Lars Hupel:


> Dear list,
> it appears that 'value' sometimes performs a (silent) fallback on other
> evaluators if something goes wrong. I don't understand the precise
> mechanics there, but one particular annoying instance is that when no
> code equations exist for some constant, 'value (code)' will leave it
> unevaluated, whereas the corresponding ML code
>   MLâCode_Evaluation.dynamic_conv @{context} @{cterm foo}â
> will print an error message
>   No code equations for foo
> It took me a while of debugging to figure out why 'value' didn't
> evaluate my term fully.
> What's the reasoning behind this?
> Cheers
> Lars


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.