PrintForm Definitions NuprlPrimitives Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sexpr size example
  Size(Cons(Inj(1);Cons(Inj(2);Inj(1)))) = 3
By: Compute Size(Cons(Inj(1);Cons(Inj(2);Inj(1)))) * 3

Generated subgoals:

None

About:
natural_numberequalmarked_clause_thenmarkup_tag
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions NuprlPrimitives Sections NuprlLIB Search Doc