Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I
am having trouble using the greater capabilities of code_identifier. I would like to
assign a constant to a different module, say
code_identifier constant replicate \<rightharpoonup> (SML) "My_Module.rep"
Then, code generation works fine as long as there is no module_name involved:
definition test where "test = replicate"
export_code test in SML
export_code test in SML module_name foo (* fails due to module dependency
cycles *)
Unfortunately, many idioms internally use module_name -- for example, all of the following
raise errors due to module dependency cycles:
ML {* @{code test} *}
value [code] "test 3 (0 :: nat)"
lemma "test = foo" quickcheck
The same problem also occurs with type constructors. Therefore: What is the intended way
of using code_identifier with constants?
Best,
Andreas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
