Glossary

a | b | c | d | e | f | g | h | i | l | o | p | q | r | s | t | u | w

	a
	attribute
	alpha-convertible
	algebraic universe
	b
	boolean attribute
	branching
	backtracking
	backtracking point
	backward reasoning
	c
	command
	convertible
	conclusion
	d
	de Bruijn criterion
	definitional equality
	e
	existential variable
	equality
	f
	flag
	first success
	forward reasoning
	g
	goal
	global environment
	h
	hypothesis
	i
	inhabited
	l
	left associative
	local context
	Leibniz equality
	o
	option
	occurrence
	p
	prelude
	proposition
	proof mode
	proof state
	proof term
	q
	quotient set
	quotient
	r
	right associative
	s
	standard library
	sentence
	sort
	strict proposition
	subgoal
	shelved
	setoid equality
	setoid
	t
	term
	type
	tactic
	table
	u
	unshelved
	w
	well-typed
	witness