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

[Ronny Wichers Schreur <ronny@xxxxxxxx>]

Hello Cesar,

You write:
> 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.

I get the same behaviour with a user-defined type (see below).


Cheers,

Ronny Wichers Schreur

--------------------------------------
typepred: THEORY
BEGIN
     T: TYPE = {MinusOne, Zero, One}

     ordinal (t:T): nat
         =   CASES t OF
                 MinusOne: 0,
                 Zero: 1,
                 One: 2
             ENDCASES

     ;< (x,y: T): bool
         =    ordinal (x) < ordinal (y)
     ;>=(x,y: T): bool
         =    ordinal (x) >= ordinal (y)

     natT: NONEMPTY_TYPE = {x: T | x >= Zero} CONTAINING Zero
     belowT(i: T): TYPE = {s: T | s < i}  % may be empty

     natL: LEMMA
         FORALL (n: natT):
             n >= Zero

     belowL: LEMMA
         FORALL (n: belowT (One)):
             n >= Zero

END typepred
--------------------------------------