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

`To follow up, Mark Wassell pointed out to me that changing the
``definition of my_nat to
`
typedef my_nat = "{ n :: nat . True }" by auto

`causes code generation to work as expected. It seems that, as part of
``the above definition, a lemma
`
Rep_my_nat: "Rep_my_nat (Abs_my_nat ?x) ≡ ?x"
is generated and used as a code equation, allowing extraction to work.
The declaration in my original example
typedef my_nat = "UNIV :: (nat) set" ..

`also causes a lemma of the same name to be generated, but of a very
``different form, which presumably can't be used as a code equation, hence
``my issues:
`
Rep_my_nat: "Rep_my_nat ?x \in UNIV"

`If I prove the lemma generated by Mark's definition myself and declare
``it as [code], extraction works as desired. Does anyone have any insight
``as to why these two typedef forms have different behaviour here?
`
Best wishes
Conrad
On 2021-06-12 11:41, C.A. Watt wrote:

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

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