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 infineon.com <Primrose.Mbanefo at infineon.com>
primrec stands for primitive recursion and needs to see all the
constructors of the datatype on the left hand side of the "=" sign.
Function (constructor1) = (do sthg)
Function (constructor2) = (do sthg)
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