# [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.*