WhoCites Definitions num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites int nzero?
int_nzeroDef  == {i:i  0 }
Thm*   Type
nequalDef a  b  T == a = b  T
Thm* A:Type, x,y:A. (x  y Prop
notDef A == A  False
Thm* A:Prop. (A Prop

Syntax: has structure: int_nzero

About:
intnatural_numbersetuniverseequalmember
propimpliesfalseall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions num thy 1 Sections StandardLIB Doc