Glossary

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


	a
	`algebraic universe`
	`alpha-convertible`
	`attribute`

	b
	`backtracking`
	`backtracking point`
	`backward reasoning`
	`beta-redex`
	`beta-reduction`
	`body`
	`boolean attribute`
	`branching`

	c
	`Calculus of Inductive Constructions`
	`command`
	`conclusion`
	`cone expression`
	`constant`
	`context-local definition`
	`contraction`
	`convertible`

	d
	`de Bruijn criterion`
	`definitional equality`
	`delta-reduction`
	`dependent premise`
	`dependent product`

	e
	`equality`
	`eta-expansion`
	`existential variable`
	`expansion`

	f
	`field`
	`first success`
	`flag`
	`focus`
	`forward reasoning`

	g
	`global environment`
	`goal`

	h
	`head`
	`head constant`
	`hole`
	`hypothesis`

	i
	`implicit argument`
	`induction principle`
	`inductive parameter`
	`inductively defined proposition`
	`inhabited`
	`iota-reduction`

	l
	`left associative`
	`Leibniz equality`
	`library`
	`load path`
	`local context`
	`logical name`
	`logical path`
	`lonely notation`

	n
	`non-dependent premise`
	`non-dependent product`
	`notation scope`

	o
	`occurrence`
	`opaque`
	`option`

	p
	`package`
	`physical path`
	`plugin`
	`prelude`
	`premise`
	`product`
	`projection`
	`proof mode`
	`proof state`
	`proof term`
	`proposition`

	q
	`quotient`
	`quotient set`

	r
	`records`
	`reduction`
	`reversible coercion`
	`right associative`

	s
	`section-local definition`
	`sentence`
	`setoid`
	`setoid equality`
	`shelved`
	`sort`
	`standard library`
	`strict proposition`
	`subgoal`

	t
	`table`
	`tactic`
	`term`
	`transparent`
	`type`

	u
	`unfold`
	`uniform inheritance condition`

	v
	`variable`

	w
	`weak-head normal form`
	`well-typed`
	`witness`

	z
	`zeta-reduction`