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

[PVS-Help] problems with an uncertainty number of parameters in functions

I define a theory about predicates as follows:
predicates[Vars: TYPE]: THEORY
     Predicate: TYPE+=[Vars -> boolean]
     and(p:Predicate, q:Predicate): Predicate = LAMBDA (v: Vars): p(v) and q(v)   
END predicates
I get a problem on how to use this theory. The number of variables in predicates can be different.
I mean if I define the theory in this way, I can not handle the predicates with two or more variables.
What can I do to it? Is this a wrong way to cope  with predicates?
Really appreciate!
Thank you!

huangchao via foxmail