Def	l	[tvar]
Def	l	[tfvar]
Def	trace(l)	[ttrace]
Def	l'	[tpvar]
Def	f	[topr]
Def	t1 t2	[tapp]
Def	term_iterate(v; p; op; f; tr; a; t)	[term_iterate]
Def	t	[typ]
Def	tTop	[st_top]
Def	ab	[arrow]
Def	t.fun	[sig_fun]
Def	t.lbl	[dec_lbl]
Def	t.typ	[dec_typ]
Def	mk_dec(lbl, typ)	[mk_dec]
Def	Case lbl : typ = > body(lbl;typ)	[case_mk_dec]
Def	t.lbl	[smt_lbl]
Def	t.term	[smt_term]
Def	t.typ	[smt_typ]
Def	mk_smt(lbl, term, typ)	[mk_smt]
Def	relname_eq(x)	[relname_eq]
Def	relname_other(x)	[relname_other]
Def	mk_rel(name, args)	[mk_rel]
Def	t.kind	[eff_kind]
Def	t.typ	[eff_typ]
Def	t.smt	[eff_smt]
Def	t.var	[frame_var]
Def	t.typ	[frame_typ]
Def	t.acts	[frame_acts]
Def	t.kind	[pre_kind]
Def	t.rel	[pre_rel]
Def	ioa_all(I; i.A(i))	[ioa_all]
Def	tc1(r;de)	[tc1]
Def	rel_arg_typ(rn;i;de)	[rel_arg_typ]
Def	tappend(tr;a)	[tappend]
Def	st_lift(rho)	[st_lift]
Def	Fmla	[pred]
Def	P Q	[pred_and]
Def	r	[pred_rel]
Def	term_vars(t)	[term_vars]
Def	P Q	[iff]	core
Def	P Q	[implies]	core
Def	Prop	[prop]	core
Def	x:A. B(x)	[all]	core
Def	f o g	[compose]	fun 1
Def	unzip(as)	[unzip]	mb list 1
Def	map(f;as)	[map]	list 1
Def	SQType(T)	[sq_type]	sqequal 1
Def	(a=b)	[ts_eq]
Def	Term	[term]
Def	SimpleType	[st]
Def	trace_env(d)	[trace_env]
Def	Decl	[decl]	mb declaration
Def	ts()	[ts]
Def	(d)	[sigma]	mb record
Def	Label	[lbl]	mb label
Def	b	[assert]	bool 1
Def	st_eq(s1;s2)	[st_eq]
Def	niltrace()	[niltrace]
Def	[[t]] e s a tr	[term_mng]
Def	apply_alist(as;l;d)	[apply_alist]
Def	(x l)	[l_member]	mb list 1
Def	P Q	[or]	core
Def	if b t else f fi	[ifthenelse]	bool 1
Def		[nat]	int 1
Def	AB	[le]	core
Def	A	[not]	core
Def	ts_case(x) var(a)= > v(a) var'(b)= > p(b) opr(f)= > op(f) fvar(x)= > f(x) trace(P)= > t(P) end_ts_case	[ts_case]
Def	Case ts_trace(x) = > body(x) cont	[case_ts_trace]
Def	Case ts_fvar(x) = > body(x) cont	[case_ts_fvar]
Def	Case ts_op(x) = > body(x) cont	[case_ts_op]
Def	Case ts_pvar(x) = > body(x) cont	[case_ts_pvar]
Def	l1 = l2	[eq_lbl]	mb basic
Def	Case x = > body(x) cont	[case_relname_other]
Def	l[i]	[select]	list 1
Def	ground_ptn(p)	[ground_ptn]	mb basic
Def	Case ptn_var(x) = > body(x) cont	[case_ptn_var]	mb basic
Def	Case ptn_int(x) = > body(x) cont	[case_ptn_int]	mb basic
Def	nth_tl(n;as)	[nth_tl]	list 1
Def	tl(l)	[tl]	list 1
Def	hd(l)	[hd]	list 1
Def	inl(x) = > body(x) cont	[case_inl]	prog 1
Def	inr(x) = > body(x) cont	[case_inr]	prog 1
Def		[it]	core
Def	t_iterate(l;n;t)	[t_iterate]	mb tree
Def	Default = > body	[case_default]	prog 1
Def	Case ts_var(x) = > body(x) cont	[case_ts_var]
Def	Case(value) body	[case]	prog 1
Def	false	[bfalse]	bool 1
Def	Tree(E)	[tree]	mb tree
Def	ts_var(x)	[ts_var]
Def	tree_leaf(x)	[tree_leaf]	mb tree
Def	ts_fvar(x)	[ts_fvar]
Def	ts_trace(x)	[ts_trace]
Def	ts_pvar(x)	[ts_pvar]
Def	ts_op(x)	[ts_op]
Def	tree_node( < x, y > )	[node]	mb tree
Def	Unit	[unit]	core
Def	true	[btrue]	bool 1
Def	Case tree_leaf(x) = > body(x) cont	[case_tree_leaf]	mb tree
Def	pq	[band]	bool 1
Def	Case x;y = > body(x;y) cont	[case_node]	mb tree
Def	Y	[ycomb]	core
Def	t.eff	[ioa_eff]
Def	t.pre	[ioa_pre]
Def	t.init	[ioa_init]
Def	t.da	[ioa_da]
Def	t.ds	[ioa_ds]
Def	t.name	[rel_name]
Def	tre.P	[tproj]
Def	t.trace	[trace_env_trace]
Def	tr | P	[trace_projection]	mb events
Def	kind(a)	[kind]	mb record
Def	1of(t)	[pi1]	core
Def	t.frame	[ioa_frame]
Def	t.rel	[sig_rel]
Def	t.args	[rel_args]
Def	t.proj	[trace_env_proj]
Def	2of(t)	[pi2]	core
Def	i:I. C(i)	[col_union]	mb collection
Def	mk_ioa(ds, da, init, pre, eff, frame)	[mk_ioa]
Def	False	[false]	core
Def	||as||	[length]	list 1
Def	Case eq(x) = > body(x) cont	[case_relname_eq]
Def		[bool]	bool 1
Def	mk_trace_env(trace, proj)	[mk_trace_env]
Def	as @ bs	[append]	list 1
Def	r.l	[r_select]	mb record
Def	Top	[top]	core
Def	Collection(T)	[col]	mb collection
Def	a + b	[col_add]	mb collection
Def	< x >	[col_singleton]	mb collection
Def	(first x as s.t. P(x) else d)	[find]	mb list 1
Def	P Q	[rev_implies]	core
Def	Pattern	[ptn]	mb basic
Def	Case ptn_pr( < x, y > ) = > body(x;y) cont	[case_lbl_pair]	mb basic
Def	x=yAtom	[eq_atom]	bool 1
Def	i=j	[eq_int]	bool 1
Def	Case ptn_atom(x) = > body(x) cont	[case_ptn_atom]	mb basic
Def	tree_con(E;T)	[tree_con]	mb tree
Def	tree_node(x)	[tree_node]	mb tree
Def	x c	[col_member]	mb collection
Def	decl_type(d;x)	[decl_type]	mb declaration
Def	filter(P;l)	[filter]	mb list 1
Def	ptn_con(T)	[ptn_con]	mb basic
Def	ij	[le_int]	bool 1
Def	reduce(f;k;as)	[reduce]	list 1
Def	i < j	[lt_int]	bool 1
Def	b	[bnot]	bool 1

About: