Def		a[i..j]	[array_seg]	array 1
Def		a[++i]	[array_shift]	array 1
Def		arr1 @ arr2	[array_append]	array 1
Def		For{T,op,id} x  as. f(x)	[for]	list 1
Def		ForHdTl{A,f,k} h::t  as. g(h;t)	[for_hdtl]	list 1
Def		mapc(f)	[mapc]	list 1
Def		Default => body EndSwitch	[switch_default]	prog 1
Def		Case(value) body	[case]	prog 1
Def		Default => body	[case_default]	prog 1
Def		<x,y> => <x,ybody(x;y)	[case_pair]	prog 1
Def		inl(x) => inl(body(x) cont	[case_inl]	prog 1
Def		inr(x) => inr(body(x) cont	[case_inr]	prog 1
Def		x::y => x::ybody(x;y) cont	[case_cons]	prog 1
Def		[] => [] =body cont	[case_nil]	prog 1
Def		=>  =>body	[case_it]	prog 1
Def		x:body	[case_bind]	prog 1
Def		<<"a", b>, c, 1> => <<"abody(b;c) cont	[case_pattern1]	prog 1
Def		<a, inl <<"a", b>, c, 1>> => <a, body(a;b;c) cont	[case_pattern2]	prog 1
Def		<a, inl <<"a", b>, c, 1>>	[pattern2]	prog 1
Def		union1()	[union1]	prog 1
Def		union1_term1(x) => uniobody(x) cont	[case_union1_term1]	prog 1
Def		union1_term1(x)	[union1_term1]	prog 1
Def		union1_term2(x) => uniobody(x) cont	[case_union1_term2]	prog 1
Def		union1_term2(x)	[union1_term2]	prog 1
Def		union1_term3(x) => uniobody(x) cont	[case_union1_term3]	prog 1
Def		union1_term3(x)	[union1_term3]	prog 1
Def		enum1_switch(value;el1;el2;el3)	[enum1_switch]	prog 1
Def		enum1_el1 => enumbody cont	[case_enum1_el1]	prog 1
Def		enum1_el2 => enumbody cont	[case_enum1_el2]	prog 1
Def		enum1_el3 => enumbody cont	[case_enum1_el3]	prog 1
Def		module1_type(prop)	[module1_type]	prog 1
Def		t.tag	[module1_tag]	prog 1
Def		t.data	[module1_data]	prog 1
Def		module1(tag, data) => modubody(tag;data)	[case_module1]	prog 1
Def		module1(tag, data)	[module1]	prog 1
Def		StAntiSym(T;x,y.R(x;y))	[st_anti_sym]	rel 1
Def		Irrefl(T;x,y.E(x;y))	[irrefl]	rel 1
Def		outl(x)	[outl]	union
Def		outr(x)	[outr]	union
Def		pq	[bxor]	bool 1
Def		pq	[rev_bimplies]	bool 1
Def		i  j  k	[lele]	int 1
Def		S  T	[suptype]	int 1
Def		Top	[top]	core
Def		t  ...$L	[label]	core
Def		???	[error]	core
Def		A & B	[cand]	core
Def		I	[icomb]	core
Def		K	[kcomb]	core
Def		S	[scomb]	core
Def		let x,y,z = a in t(x;y;z)	[spread3]	core
Def		let w,x,y,z = a in t(w;x;y;z)	[spread4]	core
Def		let a,b,c,d,e = u in v(a;b;c;d;e)	[spread5]	core
Def		let a,b,c,d,e,f = u in v(a;b;c;d;e;f)	[spread6]	core
Def		let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g)	[spread7]	core
Def		XM	[xmiddle]	core
Def		let x = a in b(x)	[let]	core
Def		[x]{T}	[type_inj]	core
Def		[T]Array{i..j}	[p_array]	array 1
Def		a +q b	[qadd]	rat 1
Def			[rat]	rat 1
Def		a *q b	[qmul]	rat 1
Def		a =q b	[eq_rat]	rat 1
Def		i =  j	[pm_equal]	int 2
Def		|i|	[absval]	int 2
Def		Preorder(T;x,y.R(x;y))	[preorder]	rel 1
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		gcd(a;b)	[gcd]	num thy 1
Def		x:A. B(x)	[sq_exists]	core
Def		CoPrime(a,b)	[coprime]	num thy 1
Def		SqStable(P)	[sq_stable]	core
Def		atomic(a)	[atomic]	num thy 1
Def		prime(a)	[prime]	num thy 1
Def		a = b mod m	[eqmod]	num thy 1
Def		fib(n)	[fib]	num thy 1
Def		null(as)	[null]	list 1
Def		ij	[ge]	core
Def		{i...j}	[int_iseg]	int 1
Def		rev(as)	[reverse]	list 1
Def		as[m..n]	[segment]	list 1
Def		l[i]	[select]	list 1
Def		as\[i]	[reject]	list 1
Def		f{m..n}	[listify]	list 1
Def		A List(n)	[list_n]	list 1
Def		i>j	[gt]	core
Def		{...i}	[int_lower]	int 1
Def		imin(a;b)	[imin]	int 2
Def		a -- b	[ndiff]	int 2
Def		Rem(a;n;r)	[rem_nrel]	int 2
Def		a mod n	[modulus]	int 2
Def		a  n	[div_floor]	int 2
Def		WellFnd{i}(A;x,y.R(x;y))	[wellfounded]	well fnd
Def		FIncr	[fincr]	rfunction 1
Def		enum1()	[enum1]	prog 1
Def		SQType(T)	[sq_type]	sqequal 1
Def		x=yAtom	[eq_atom]	bool 1
Def		Symmetrize(x,y.R(x;y);a;b)	[symmetrize]	rel 1
Def		IsEqFun(T;eq)	[eqfun_p]	rel 1
Def		strict_part(x,y.R(x;y);a;b)	[strict_part]	rel 1
Def		Linorder(T;x,y.R(x;y))	[linorder]	rel 1
Def		isl(x)	[isl]	union
Def		b2i(b)	[b2i]	bool 1
Def		p=q	[eq_bool]	bool 1
Def		Bij(A; B; f)	[biject]	fun 1
Def		A ~~ B	[one_one_corr]	fun 1
Def		Stable{P}	[stable]	core
Def		{a:T}	[singleton]	core
Def		{!x:T | P(x)}	[unique_set]	core
Def		a = !x:T. Q(x)	[uni_sat]	core
Def		[T]Array	[array]	array 1
Def		{i..j}	[int_seg]	int 1
Def		{i...}	[int_upper]	int 1
Def		a.u	[array_ub]	array 1
Def		a.l	[array_lb]	array 1
Def		q.num	[qnumer]	rat 1
Def		1of(t)	[pi1]	core
Def		a[i]	[array_el]	array 1
Def		q.den	[qdenom]	rat 1
Def		2of(t)	[pi2]	core
Def		P & Q	[and]	core
Def			[nat_plus]	int 1
Def		Case v => case cont	[switch_case]	prog 1
Def		i=j	[eq_int]	bool 1
Def		p/q	[qnum]	rat 1
Def		x:A. B(x)	[exists]	core
Def		GCD(a;b;y)	[gcd_p]	num thy 1
Def		reducible(a)	[reducible]	num thy 1
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def		P  Q	[implies]	core
Def		x:A. B(x)	[all]	core
Def		if b t else f fi	[ifthenelse]	bool 1
Def		Y	[ycomb]	core
Def			[int_nzero]	int 1
Def		Div(a;n;q)	[div_nrel]	int 2
Def		i  j < k	[lelt]	int 1
Def			[nat]	int 1
Def		AB	[le]	core
Def		a  b	[nequal]	core
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def		P  Q	[or]	core
Def		pq	[bimplies]	bool 1
Def		p  q	[bor]	bool 1
Def		false	[bfalse]	bool 1
Def		true	[btrue]	bool 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		tl(l)	[tl]	list 1
Def		imax(a;b)	[imax]	int 2
Def		ij	[le_int]	bool 1
Def		as @ bs	[append]	list 1
Def		firstn(n;as)	[firstn]	list 1
Def		i<j	[lt_int]	bool 1
Def		hd(l)	[hd]	list 1
Def		x:T. b(x)	[tlambda]	fun 1
Def		map(f;as)	[map]	list 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		mapcons(f;as)	[mapcons]	list 1
Def		||as||	[length]	list 1
Def		<<"a", b>, c, 1>	[pattern1]	prog 1
Def			[bool]	bool 1
Def		EndSwitch	[switch_done]	prog 1
Def		enum1_el3	[enum1_el3]	prog 1
Def		enum1_el2	[enum1_el2]	prog 1
Def		enum1_el1	[enum1_el1]	prog 1
Def		Switch(t) b	[switch]	prog 1
Def		Unit	[unit]	core
Def		{T}	[guard]	core
Def		Order(T;x,y.R(x;y))	[order]	rel 1
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		x f y	[infix_ap]	core
Def		b	[assert]	bool 1
Def		P  Q	[iff]	core
Def		AntiSym(T;x,y.R(x;y))	[anti_sym]	rel 1
Def		Connex(T;x,y.R(x;y))	[connex]	rel 1
Def			[it]	core
Def		False	[false]	core
Def		True	[true]	core
Def		b	[bnot]	bool 1
Def		pq	[band]	bool 1
Def		S  T	[subtype]	core
Def		Prop	[prop]	core
Def		InvFuns(A; B; f; g)	[inv_funs]	fun 1
Def		Id	[tidentity]	fun 1
Def		Id	[identity]	fun 1
Def		f o g	[compose]	fun 1
Def		Surj(A; B; f)	[surject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		P  Q	[rev_implies]	core
Def		T	[squash]	core

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