Index of types


E
envs [AAC_theory.Trans]
ext_units [AAC_matcher]

G
goal_sigma [AAC_coq]

H
hypinfo [AAC_coq.Rewrite]
We keep some informations about the hypothesis, with an (informal) invariant: typeof hyp = typ, typ = forall context, body, body = rel left right

I
ir [AAC_theory.Trans]

M
m [AAC_search_monad]
A data type that represent a collection of 'a
mset [AAC_matcher]
The arguments of sums (or AC operators) are represented using finite multisets.

N
nf_term [AAC_matcher.Terms]

P
pack [AAC_theory.Sym]
mimics the Coq record Sym.pack

R
reifier [AAC_theory.Trans]
We need to reify two terms (left and right members of a goal) that share the same reification envirnoment.

S
sigmas [AAC_theory.Trans]
symbol [AAC_matcher]

T
t [AAC_matcher.Subst]
t [AAC_matcher.Terms]
t [AAC_coq.Equivalence]
t [AAC_coq.Transitive]
t [AAC_coq.Relation]

U
units [AAC_matcher]

V
var [AAC_matcher]