Re: [isabelle] List construction



Hello,
I tried to use the constructors only in the left hand (how I read in the
tutorial) but Isabelle tell me that there are many non-variable terms in
lhs.

However I resolved the problem using recdef.

Thanks and best regards
Gabriele

On 10/4/06, Primrose.Mbanefo at infineon.com <Primrose.Mbanefo at infineon.com>
wrote:

primrec stands for primitive recursion and needs to see all the
constructors of the datatype on the left hand side of the "=" sign.

I mean:
Function (constructor1) = (do sthg)
Function (constructor2) = (do sthg)

you did:
Function eqn = if constructor1 (do sthg) else if constructor2 (do sthg)
...

you put the two constructors together in the same statement so primrec
cannot find them.
Split the statment into:
primrec
"emptyRes2aux () 0 = []"
"emptyRes2aux () Suc h = free # emptyRes2aux () h"


to use the two constructors in one, try recdef instead.





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