Who Cites hinr?
hinr	Def inr == x:'b. inr(x)
	Thm* 'b,'a:S. inr  ('b  hsum('a; 'b))
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

inr

has structure:

hinr('b; 'a)

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