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



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




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