Email Gateway (Aug 18 2022 at 10:37): Email Gateway (Aug 18 2022 at 10:37):From: Alexander Krauss <krauss@in.tum.de>
Hi Peter,
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?
Alex
Email Gateway (Aug 18 2022 at 10:41):From: Peter Chapman <pc@cs.st-and.ac.uk>
Hi
I've got a function which takes two lists and a formula, and returns
a formula, i.e.
absMany :: "'a list => 'b list => form => form"
which I want to have the following behaviour (the two middle cases
will never be used, since I want to use the function only after I've
enforced length X = length Y)
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
second argument.
I've also tried coming at it from another angle, so that
absMany :: " 'a list => form => form"
and "hiding" the second list in the formula, but again in the crucial
case where both lists are non-empty I cannot break both lists down to
talk of an expression involving x,y, xs and ys.
I looked into mutual recursion, but because the datatypes are not
mutually recursive, I didn't think it was applicable.
Does anyone know how to do this properly?
Cheers
Peter
Last updated: May 03 2024 at 12:27 UTC