Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with HOL-Library.Code_Char

view this post on Zulip Email Gateway (Aug 22 2022 at 16:47):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

we currently have a problem that generated Haskell code does not compile
if we load theory “HOL-Library.Code_Char”.

The problem only occurs for Haskell and not for Scala, SML, OCaml, ...

Minimal Example:

theory Bug
imports
Main
"HOL-Library.Code_Char"
begin

definition foo where "foo = [0]"

export_code foo in Haskell

(* results in

foo :: forall a. (Arith.Zero a) => [a];
foo = "\^@";

and not in

foo :: forall a. (Arith.Zero a) => [a];
foo = [Arith.zero];

*)

end

With best regards,
René

view this post on Zulip Email Gateway (Aug 22 2022 at 16:51):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
For the record: this has been resolved in 3817a93a3e5e.

Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC