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

RE: [PVS-Help] Showing all type predicates for a skolem constant



Title: RE: [PVS-Help] Showing all type predicates for a skolem constant

Maybe not. Numbers are part of the PVS prelude and they are built-in. It may be that the strategy all-typepreds only displays user defined type predicates. I'm not sure how to get the implicit predicate N >= 0.

Cesar

-----Mensaje original-----
De: pvs-help-bounces+munoz=nianet.org@csl.sri.com en nombre de Ronny Wichers Schreur
Enviado el: Vie 12/15/2006 3:11 p.m.
Para: Cesar Munoz
CC: pvs-help@csl.sri.com
Asunto: Re: [PVS-Help] Showing all type predicates for a skolem constant

Hell Cesar,

Thanks for your help. You write:

> There is a strategy in PVS called all-typepreds that is supposed to do
> that. However, in your example, we get everything but N >= 0:

So is this a bug?


Cheers,

Ronny Wichers Schreur