Some definitions of interest.
msga	Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop
	Thm* MsgA  Type{i'}
assert	Def b == if b True else False fi
	Thm* b:. b  Prop
ma-empty	Def  == mk-ma(; ; ; ; ; ; ; )
ma-is-empty	Def ma-is-empty(M) Def == fpf-is-empty(1of(M))fpf-is-empty(1of(2of(M))) Def == fpf-is-empty(1of(2of(2of(M))))fpf-is-empty(1of(2of(2of(2of(M))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(M)))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(M))))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(M)))))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(2of(M)))))))))

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