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)

it returns

[](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 ?

Thank you.

Just to clarify, I am using the next translation for the operators

Box []

Plus +

Implies =>