Re: [isabelle] nat_code Equation

Hi René,

>> Note that if you import HOL/Library/Code_Nat.thy, which declares a
>> binary code representation for type nat, then the implementation of
>> function nat from Code_Integer is *much* faster than either nat' or
>> nat_th.
> Perhaps, then one can load this more complex nat-function only in "HOL/Library/Code_Nat.thy"?

the observation made by Brian has indeed been the primary motiviation
for this »representation-ignorant binary digit scanning« equation.
There is a high chance that this could be changed in a similar way you
suggest.  However, there is a reform of all that code generation
arithmetic stuff ongoing, and this particular issue cannot be dealt in
isolation with within the distribution.  So, I would recommend to
declare this code equation in your particular application until this
reform shows up in a release (it is very likely that this will not be
the upcoming release).

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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