FDL
>
PVS
>
Prelude
>
integers
> posnat
: nonempty-type-eq-decl
posnat : NONEMPTY_TYPE =
posint