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.
De: email@example.com en nombre de Ronny Wichers Schreur
Enviado el: Vie 12/15/2006 3:11 p.m.
Para: Cesar Munoz
Asunto: Re: [PVS-Help] Showing all type predicates for a skolem constant
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?
Ronny Wichers Schreur