[isabelle-dev] HOL-Codegenerator_Test error

[Manuel Eberl]

There are actually several affected functions:

Discrete.sqrt
size_fset
lapprox_posrat
size_multiset
set_encode
card_UNIV_fun
card_UNIV_set
card_UNIV_finfun


I have no idea what causes this and why my changed affected it. I also 
do not have the faintest idea what I could possibly do to fix it. I also 
do not understand why "export_code … checking" puts everything in a 
single module and if that perhaps has anything to do with it. If I 
simply do "export_code" (without "checking" and "module_name"), the 
problem does /not/ occur. (another completely different problem occurs, 
something about implicits and Typereps)

 From what I have seen so far, it seems like there are some lingering 
issues with code generation in general and Codegenerator_Test in 
particular that my rather innocuous change exposed, and that simply 
deleting that one code equation that I added is not the solution we want 
(not even in the short term).

Moreover, at least one AFP entry (namely Rene Thiemann's 
Algebraic_Numbers) crucially depends on a similar code equation for 
"binomial", which causes the exact same problem. We could just leave 
this orphaned code equation in the AFP for now, but that does not strike 
me as a good solution either.


Cheers,

Manuel