Def		xL.P(x)	[list_exists_2]	list 3 jlc
Def		T	[theta]	lambda jlc
Def		Y	[applicative_Y]	lambda jlc
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 > = > body(x;y)	[case_pair]	prog 1
Def		inl(x) = > body(x) cont	[case_inl]	prog 1
Def		inr(x) = > body(x) cont	[case_inr]	prog 1
Def		x::y = > body(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 > = > body(b;c) cont	[case_pattern1]	prog 1
Def		< a, inl < < "a", b > , c, 1 > > = > 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) = > body(x) cont	[case_union1_term1]	prog 1
Def		union1_term1(x)	[union1_term1]	prog 1
Def		union1_term2(x) = > body(x) cont	[case_union1_term2]	prog 1
Def		union1_term2(x)	[union1_term2]	prog 1
Def		union1_term3(x) = > body(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 = > body cont	[case_enum1_el1]	prog 1
Def		enum1_el2 = > body cont	[case_enum1_el2]	prog 1
Def		enum1_el3 = > body 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) = > body(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		x:A. B(x)	[sq_exists]	core
Def		Top	[top]	core
Def		t ...$L	[label]	core
Def		???	[error]	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		||	[list_length]	list 3 jlc
Def		ij	[ge]	core
Def		Discrete{T}	[discrete]	discrete jlc
Def		null(as)	[null]	list 1
Def		remove(eq;x;L)	[remove]	list 3 jlc
Def		filter(f;L)	[filter]	list 3 jlc
Def		SqStable(P)	[sq_stable]	core
Def		{T}	[equivalence]	core 3 jlc
Def		{T=}	[discrete_equality]	discrete jlc
Def		disjoint(eq;L1;L2)	[disjoint]	list 3 jlc
Def		disjoint(eq;L;M)	[disjoint2]	list 3 jlc
Def		A & B	[cand]	core
Def		L1(~eq)L2	[list_iso]	list 3 jlc
Def		(~eq)	[list_iso_2]	list 3 jlc
Def		L(eq)M	[is_intersection]	list 3 jlc
Def		p=q	[eq_bool]	bool 1
Def		curry f	[curry]	lambda jlc
Def		uncurry f	[uncurry]	lambda jlc
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			[nat_plus]	int 1
Def			[int_nzero]	int 1
Def		i > j	[gt]	core
Def		|i|	[absval]	int 2
Def		{...i}	[int_lower]	int 1
Def		i = j	[pm_equal]	int 2
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		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		Symmetrize(x,y.R(x;y);a;b)	[symmetrize]	rel 1
Def		Preorder(T;x,y.R(x;y))	[preorder]	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		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		L1(eq)L2	[sublist]	list 3 jlc
Def		(eq)	[sublist_2]	list 3 jlc
Def		x(eq) L	[is_member]	list 3 jlc
Def		xL.P(x)	[list_all]	list 3 jlc
Def		xL.P(x)	[list_all_2]	list 3 jlc
Def		xL.P(x)	[list_exists]	list 3 jlc
Def		= b	[letrec_body]	lambda jlc
Def		x b(x)	[letrec_arg]	lambda jlc
Def		(letrec f b(f))	[letrec]	lambda jlc
Def		if b t else f fi	[ifthenelse]	bool 1
Def		true	[btrue]	bool 1
Def		false	[bfalse]	bool 1
Def		P & Q	[and]	core
Def		True	[true]	core
Def		pq	[band]	bool 1
Def		P Q	[or]	core
Def		False	[false]	core
Def		pq	[bimplies]	bool 1
Def		p q	[bor]	bool 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		imax(a;b)	[imax]	int 2
Def		ij	[le_int]	bool 1
Def		b	[bnot]	bool 1
Def		b	[assert]	bool 1
Def		P Q	[implies]	core
Def		P Q	[iff]	core
Def		x:A. B(x)	[all]	core
Def			[bool]	bool 1
Def		Dec(P)	[decidable]	core
Def		Y	[ycomb]	core
Def		tl(l)	[tl]	list 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		Div(a;n;q)	[div_nrel]	int 2
Def		{i..j}	[int_seg]	int 1
Def		i j < k	[lelt]	int 1
Def			[nat]	int 1
Def		x:A. B(x)	[exists]	core
Def		Case v = > case cont	[switch_case]	prog 1
Def		i=j	[eq_int]	bool 1
Def		{i...}	[int_upper]	int 1
Def		< < "a", b > , c, 1 >	[pattern1]	prog 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		1of(t)	[pi1]	core
Def		2of(t)	[pi2]	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		AB	[le]	core
Def		a b	[nequal]	core
Def		A	[not]	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		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: