Re: [isabelle] nat_code Equation

Hi all,

>> Thanks Brian, for the new version of Code_Nat.

see now

It is now possible, in theory Code_Binary_Nat, to drop the dependency on
the venerable preprocessor by Stefan Berghofer (theory
Code_Abstract_Nat) and install this specific preprocessor instead.

> However, after some more thought I don't think that my general
> approach will work at all for patterns like "Suc (Suc n)"; in the long
> run we'll probably have to stay with a code preprocessor like the
> current one, which can combine multiple equations into single ones
> that use if-then-else or case.

Also the preprocessor from Code_Abstract_Nat cannot compile away all
patterns: it always needs 0/Suc twins to proceed.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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