[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
union variable binding operator
I'm pretty sure that PVS has a variable binding operator for unions (or
a function from set&function pairs to sets), like there is for summing:
sum(S: set, f:[S -> int])
but I can't find it... Isn't there such a thing?
I.e. an operator 'union' so that where R is some set of sets
union(S: set, f: [S -> set]) = | | f(x)
forall x in S
Thanks, sorry if I'm missing something obvious...