[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] recursive functions calling each other



Hi there,

I have two recursive functions that call each other:

a(x: nat): RECURSIVE bool =
...
b(x)
...
MEASURE x

b(y: nat): RECURSIVE bool =
...
a(y)
...
MEASURE y

I don't know how to do this without getting resolution errors.

Thanks for your help,
Lucian