[isabelle] BUG: Imperative/HOL Code Generation Array.of_list



Hi all:

For ImperativeHOL, that comes with the Isabelle2009-1 distribution:

The SML code generator complains that it has no equations for constant
of_list'.

For SML and OCaml, there are code constants for of_list, only Haskell
declares the code_const for of_list'.
However, the code-lemmas are set up to unfold of_list to of_list'
(target independently)

Adding the missing code_const, i.e.
   code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")

solves the problem.


Regards,
  Peter





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