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
constructor
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
inhabitant
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
sort polymorphic
sort qualities
standard library
strict proposition
subgoal
 
t
table
tactic
term
transparent
type
 
u
unfold
uniform inheritance condition
 
v
variable
volatile cast
 
w
weak-head normal form
well-typed
 
z
zeta-reduction