[isabelle] Code equations for Rep in lift_definition with type constructor



Dear list

I am stuck trying to get an example to generate executable code. A stripped down version is attached. I define a type "my_nat", set up as a trivial quotient of nat. I lift a definition

  definition all_zeros :: "nat list => bool"

to

  lift_definition my_all_zeros :: "my_nat list => bool" is all_zeros .

When I attempt to export the code of the lifted function, I get the error "No code equations for Rep_my_nat".

It looks like this is caused by the code equation for my_all_zeros working out as

  my_all_zeros ?xa ≡ all_zeros (map Rep_my_nat ?xa)

Is there a way to make code generation work with this quotient/lifting setup? I found the "code_dt" flag to lift_definition, which seems to be documented in isar-ref as dealing with something vaguely related, but it doesn't affect the behaviour here.

Best wishes
Conrad Watt
theory Test imports Main begin

typedef my_nat = "UNIV :: (nat) set" ..

setup_lifting type_definition_my_nat

definition all_zeros :: "nat list \<Rightarrow> bool" where
  "all_zeros nl = list_all (\<lambda>n. n = 0) nl"

lift_definition(code_dt) my_all_zeros :: "my_nat list \<Rightarrow> bool" is all_zeros .

code_thms my_all_zeros

export_code open my_all_zeros
  in OCaml
(* Error: No code equations for Rep_my_nat *)
end


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