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

Re: Extension set declaration



At 10:49 AM 6/4/03 +0200, Frederic Dadeau wrote:
>Hello everyone,
>
>I'm looking for help on using PVS with sets.
>
>I would like to know how to instanciate sets defined in extension. For 
>example :
>how to translate this : mySet = {atom1, atom2, ..., atomN} in PVS ?
>
>I've already tried something like :
>
>T

      mySet = add(atom1,add(atom2, ..... singleton(atomN)))))))))))))))))))

or

      mySet = {x: T | x = atom1 or x = atom2 or ..... or x = atomN}


Rick