[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
sorry, slight slip in my query
Sorry, there was a slight slip in my last PVS query. Here's the question
Does PVS have a variable binding operator for unions (or a function from
set & function pairs to sets), like the one for summation?
I've looked in the Prelude and in the finite_sets library, and haven't
seen it... Isn't there such a thing?
I.e. an operator 'union' so that where S is a set, and f is a function
mapping each element of S to an element in some set of sets, R, we have
union(S: set, f: [S -> R]) = | | f(x)
forall x in S
I thought PVS came with this operation pre-defined. Thanks, sorry if I'm
missing something obvious...