Re: [isabelle] List construction

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

However I resolved the problem using recdef.

Thanks and best regards

On 10/4/06, Primrose.Mbanefo at <Primrose.Mbanefo at>

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:
"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.