(3steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc funeq example1 1

1. x : 
  x = if x<0 0 ; x fi  


By: Decide: x<0


Generated subgoal:

1 2. x<0
  x = if x<0 0 ; x fi  

1 step

About:
natural_numberlessless_thanequal
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(3steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc