Re: [isabelle] Problem analysing cases
absMany [ ] [ ] A = A
absMany (x # xs ) [ ] A = A
absMany [ ] (y # ys) A = A
absMany (x # xs) (y # ys) A = abs x (Ex y. (absMany xs ys A))
I've tried doing this via primrec, with case expressions, let
expressions and if-then-else expressions, but I can't analyse the
Primrec cannot do this kind of thing, since it only allows pattern
matching on a single argument. However, you should be able to use
recdef (or, if you happen to
have a developer's version, the new "fun" command) for this.
Alternatively, you should be able to use case expressions. What did
you try exactly, and why didn't it work?
This archive was generated by a fusion of
Pipermail (Mailman edition) and