[isabelle] Incompatibility between code generation, HOL-Library.Numeral_Type, and Containers.Set_Impl



Hi,

when importing both HOL-Library.Numeral_Type (from Isabelle) and Containers.Set_Impl (from AFP), then the code generation for computing the cardinality of "UNIV::unit set" (which should be 1) produces nonterminating code.

As shown in the attached theory, it defines a trivially diverging recursive function "fun card A_ = card A_".

If only one of those two theories is included, the generated code returns 1 immediately.

I don't understand where the recursive function comes from.

(I don't need a hotfix because this problem occurred only during experimentation. But it might be good to understand where this comes from and whether it relates to some deeper problem.)

Best wishes,
Dominique.


theory Test 
  imports
    "HOL-Library.Numeral_Type"
    Containers.Set_Impl
begin

(* Does not terminate: *)
(* value \<open>CARD(unit)\<close> *)

definition "one = CARD(unit)"
export_code "one" in SML
(* Exported code contains \<open>fun card A_ = card A_\<close> *)

end


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