Glossary

a | b | c | d | f | i | l | o | p | r | s | t | w

	a
	attribute
	alpha-convertible
	algebraic universe
	b
	branching
	backtracking
	backtracking point
	c
	command
	convertible
	d
	de Bruijn criterion
	f
	flag
	first success
	i
	inhabited
	l
	left associative
	o
	option
	p
	prelude
	proposition
	r
	right associative
	s
	standard library
	sentence
	sort
	strict proposition
	t
	term
	type
	tactic
	table
	w
	well-typed
	witness