Re: [isabelle] Sequence case

The "case" expression in Isabelle is rather restrictive: you have to list the cases in the exact same order as they appear in the corresponding datatype declaration, and _ is not allowed.

Larry Paulson

On 19 Sep 2006, at 14:41, Gabriele Pozzani wrote:

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:

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