Re: [isabelle] nat_code Equation



Hi all,

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

see now http://isabelle.in.tum.de/repos/isabelle/rev/0a2371e7ced3

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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