[isabelle] No code equations for explode on String.literal
the code generator setup for equality on String.literal seems unsatisfactory, as the
following example shows:
theory Scratch imports Main begin
definition empty :: "String.literal => bool" where "empty x = (x = STR '''')"
value [nbe] "empty (STR '''')"
declare equal_literal_def [code del] (* *** *)
value [code] "empty (STR '''')"
export_code empty in SML file -
I cannot generate code for equality tests on String.literal unless I remove the code
equation equal_literal_def in line ***. However, value [nbe] requires this equation in
order to fully evaluate terms like "empty (STR '''')". How can we have both [code] and
[nbe] work simultaneously for equality on String.literal? I tried the following, but it
the problem remains the same.
declare equal_literal_def [code del, code nbe]
Shouldn't the code generator ignore [code nbe] theorems when it checks whether there are
enough code equations?
This archive was generated by a fusion of
Pipermail (Mailman edition) and