Re: [isabelle] Sequence case
So I wrote:
consts first_occur::"('a × 'b) lift seq => 'a => 'b"
"first_occur ex a == (case ex of
x##xs => if (fst(x)=a) then snd(x) else (first_occur xs a)
| _ => arbitrary)"
But it don't work and Isabelle stops with the follow error:
*** exception TERM raised: Error in case expression:
*** Not a datatype constructor: Cfun.Rep_CFun
*** Error in parse translation for "_case_syntax"
*** At command "primrec".
Where is the problem?
Probably because "_" is not supported and the order of the cases must be
the same as in the domain definition.
This archive was generated by a fusion of
Pipermail (Mailman edition) and