[isabelle] Problem with HOL-Library.Code_Char



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Ã


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