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

Re: [PVS-HELP] Choose Function



Title:
SongFu wrote:
> Dear everyone:
> I want know how to proof the following:

> choose({x: nat| x=1}) =1

> Thanks
> Song


If you look at the definition of choose (in the prelude), you'll see
its type makes this easy.

 (typepred "choose({x: nat | x = 1})")
then
 (hide 2) (grind)

John