Re: [isabelle] code-generation Efficient_Nat

Hi Christian,

> I thought Efficient_Nat would take care of transforming an equation as
> the one causing the error into a form using 'if/then/else' instead of
> the pattern? Am I doing anything wrong, or does Efficient_Nat not work
> as expected?

In general, this procedure is not complete, c.f. »Eliminating pattern
matching on natural numbers.« on p77 in

Concerning your problem in particular,

> *** "Nat.Suc" is not a constructor, on left hand side of equation:
> *** fit_length ?a (Suc ?v) [] == replicate (Suc ?v) ?a

you should inspect the code equations for fit_length using
print_codesetup and see whether they bear a problem.  In case, you can
always replace the offending code equations manually.

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.