Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:56):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 14:56):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

thanks for reporting this. I have repaired this in the repository.

Florian
signature.asc

Last updated: Apr 20 2024 at 08:16 UTC