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:

Cheers,
	Florian

> 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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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