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] |