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