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

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



Hi,
 
I define a theory about predicates as follows:
 
predicates[Vars: TYPE]: THEORY
BEGIN
     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

huangchao via foxmail