Hi, I am trying to implement a recursive call with the next code :
| Plus (x,y) -> begin match x, y with | x, Box y -> Box (Implies(x, y)) | x, Plus (a, b) -> Plus(x, Plus(a, b)) | x, y -> Implies(x, y) end
I am now testing the code with the next two cases :
case 01 … +(p, z)
(p => z)
which is the correct translation for case 01.
case 02 … +(p,+(q, z))
it should return
(p => (q => z)) ,
instead of that, it is going inside an infinity loop.
I can see the problem is in the second line of the match, when I am calling Plus inside another Plus, but I understand the “exit” of the loop is given by the first line of the match.
Could you give me any feedback to overcome this problem ?
Just to clarify, I am using the next translation for the operators