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

*To*: pvs-help@csl.sri.com*Subject*: sorry, slight slip in my query*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Sat, 25 Sep 1999 11:41:13 -0400 (EDT)

Sorry, there was a slight slip in my last PVS query. Here's the question again, corrected: 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... Mark Aronszajn

- Prev by Date:
**union variable binding operator** - Next by Date:
**Re: union variable binding operator** - Prev by thread:
**Re: Moving existential quantifiers out over universal quantifiers** - Next by thread:
**union variable binding operator** - Index(es):