Who Cites hlet?
hlet	Def let == f:'a'b. e:'a. let x = e in f(x)
	Thm* 'a,'b:S. let  (('a  'b)  'a  'b)
let	Def let x = a in b(x) == (x.b(x))(a)
	Thm* A,B:Type, a:A, b:(AB). let x = a in b(x)  B
tlambda	Def (x:T. b(x))(x) == b(x)

Syntax:

let

has structure:

hlet('a; 'b)

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