[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Mutual recursive functions
Sjaak Smetsers writes:
F (. )(g) = . g(.).
and to replace the application of F in G's body by
G (.) = . F( .)(G) .
You need to put more information into the type, eg
F(x)(g : [(below_measure_of(x)) -> ... ]) = ...
Similarly to what you have to do for double recursion, see
f91.pvs in the Examples directory in the pvs 2.4 distribution. To
say more I need to have the sources of your problem.
A different approach for mutual recursive function is to combine
domain and codomain with the union datatype:
FG : [union[domain(F),domain(G)] -> union[codomain(F),codomain(G)]] =
lambda xy : cases xy of
inl(x) : F(x),
inr(y) : G(y)