Re: [isabelle] nat_code Equation

Hi Florian,

>>> 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).

This is perfectly fine for me. I can easily install my code-equation
and will also wait on other changes in arithmetic. Anyway, my main 
motivation for posting my observation was that if one does not know 
about Code_Nat one obtains strange-looking code for "nat".


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