Re: [isabelle] nat_code Equation

> 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"?

- René

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