[isabelle] code-generation Efficient_Nat



Hi there,

I ran into the following Problem when using Efficient_Nat

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

I am generating code by the command

$(ISABELLE_TOOL) codegen $(ISAFOR) Ceta \
'certifyProof in Haskell module_name Ceta file "../generated/Haskell/"';

where $(ISAFOR) is a Heap-Image whose last theory is Ceta.thy and the last import of Ceta.thy is Efficient_Nat.

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?

cheers

chris





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