PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /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 /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc