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)
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?
huangchao via foxmail