FDL
>
PVS
>
Prelude
>
integers
> int
: nonempty-type-eq-decl
int : NONEMPTY_TYPE =
integer