[isabelle] BUG: Imperative/HOL Code Generation Array.of_list
For ImperativeHOL, that comes with the Isabelle2009-1 distribution:
The SML code generator complains that it has no equations for constant
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'
Adding the missing code_const, i.e.
code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
solves the problem.
This archive was generated by a fusion of
Pipermail (Mailman edition) and