Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1064 entries) |
Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (489 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (119 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |
Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (104 entries) |
Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
Global Index
A
AAC [library]aac_lift_proper [instance, in AAC_tactics.AAC]
aac_lift_subrelation [instance, in AAC_tactics.AAC]
aac_list_proper [projection, in AAC_tactics.AAC]
aac_lift_equivalence [projection, in AAC_tactics.AAC]
AAC_lift [record, in AAC_tactics.AAC]
AAC_normalise.d [variable, in AAC_tactics.Tutorial]
AAC_normalise.c [variable, in AAC_tactics.Tutorial]
AAC_normalise.b [variable, in AAC_tactics.Tutorial]
AAC_normalise.a [variable, in AAC_tactics.Tutorial]
AAC_normalise [section, in AAC_tactics.Tutorial]
aac_zero_max [instance, in AAC_tactics.Tutorial]
aac_max_Idem [instance, in AAC_tactics.Tutorial]
aac_max_Assoc [instance, in AAC_tactics.Tutorial]
aac_max_Comm [instance, in AAC_tactics.Tutorial]
aac_zero_add [instance, in AAC_tactics.Tutorial]
aac_one [instance, in AAC_tactics.Tutorial]
aac_mul_Assoc [instance, in AAC_tactics.Tutorial]
aac_mul_Comm [instance, in AAC_tactics.Tutorial]
aac_add_Comm [instance, in AAC_tactics.Tutorial]
aac_add_Assoc [instance, in AAC_tactics.Tutorial]
All [module, in AAC_tactics.Instances]
appne [definition, in AAC_tactics.Utils]
Associative [record, in AAC_tactics.AAC]
Associative [inductive, in AAC_tactics.AAC]
A:1 [binder, in AAC_tactics.AAC]
A:11 [binder, in AAC_tactics.Utils]
A:156 [binder, in AAC_tactics.AAC]
A:159 [binder, in AAC_tactics.AAC]
a:16 [binder, in AAC_tactics.Caveats]
A:163 [binder, in AAC_tactics.AAC]
A:20 [binder, in AAC_tactics.Utils]
a:248 [binder, in AAC_tactics.AAC]
a:25 [binder, in AAC_tactics.Caveats]
a:28 [binder, in AAC_tactics.Caveats]
a:308 [binder, in AAC_tactics.AAC]
a:322 [binder, in AAC_tactics.AAC]
a:33 [binder, in AAC_tactics.Caveats]
a:35 [binder, in AAC_tactics.Caveats]
A:36 [binder, in AAC_tactics.Utils]
A:39 [binder, in AAC_tactics.Utils]
a:39 [binder, in AAC_tactics.Caveats]
A:4 [binder, in AAC_tactics.Instances]
A:42 [binder, in AAC_tactics.Utils]
a:46 [binder, in AAC_tactics.Caveats]
A:47 [binder, in AAC_tactics.Utils]
a:47 [binder, in AAC_tactics.Caveats]
A:5 [binder, in AAC_tactics.Instances]
A:50 [binder, in AAC_tactics.Utils]
A:53 [binder, in AAC_tactics.Utils]
A:56 [binder, in AAC_tactics.Utils]
A:6 [binder, in AAC_tactics.Instances]
A:62 [binder, in AAC_tactics.Utils]
A:67 [binder, in AAC_tactics.Utils]
A:7 [binder, in AAC_tactics.Instances]
A:76 [binder, in AAC_tactics.Utils]
A:8 [binder, in AAC_tactics.Instances]
a:84 [binder, in AAC_tactics.Tutorial]
A:9 [binder, in AAC_tactics.Instances]
B
base [section, in AAC_tactics.Tutorial]base.both [section, in AAC_tactics.Tutorial]
base.both.a [variable, in AAC_tactics.Tutorial]
base.both.b [variable, in AAC_tactics.Tutorial]
base.both.c [variable, in AAC_tactics.Tutorial]
base.both.d [variable, in AAC_tactics.Tutorial]
base.both.H [variable, in AAC_tactics.Tutorial]
base.both.H' [variable, in AAC_tactics.Tutorial]
base.dealing_with_units.H' [variable, in AAC_tactics.Tutorial]
base.dealing_with_units.H [variable, in AAC_tactics.Tutorial]
base.dealing_with_units.c [variable, in AAC_tactics.Tutorial]
base.dealing_with_units.b [variable, in AAC_tactics.Tutorial]
base.dealing_with_units.a [variable, in AAC_tactics.Tutorial]
base.dealing_with_units [section, in AAC_tactics.Tutorial]
base.morphisms [section, in AAC_tactics.Tutorial]
base.morphisms.a [variable, in AAC_tactics.Tutorial]
base.morphisms.b [variable, in AAC_tactics.Tutorial]
base.morphisms.f [variable, in AAC_tactics.Tutorial]
base.morphisms.g [variable, in AAC_tactics.Tutorial]
base.morphisms.H [variable, in AAC_tactics.Tutorial]
base.morphisms.Hf [variable, in AAC_tactics.Tutorial]
base.morphisms.Hg [variable, in AAC_tactics.Tutorial]
base.occurrence [section, in AAC_tactics.Tutorial]
base.occurrence.a [variable, in AAC_tactics.Tutorial]
base.occurrence.f [variable, in AAC_tactics.Tutorial]
base.occurrence.H [variable, in AAC_tactics.Tutorial]
base.occurrence.Hf [variable, in AAC_tactics.Tutorial]
base.reminder [section, in AAC_tactics.Tutorial]
base.reminder.a [variable, in AAC_tactics.Tutorial]
base.reminder.b [variable, in AAC_tactics.Tutorial]
base.reminder.c [variable, in AAC_tactics.Tutorial]
base.reminder.H [variable, in AAC_tactics.Tutorial]
base.subst [section, in AAC_tactics.Tutorial]
base.subst.a [variable, in AAC_tactics.Tutorial]
base.subst.b [variable, in AAC_tactics.Tutorial]
base.subst.c [variable, in AAC_tactics.Tutorial]
base.subst.d [variable, in AAC_tactics.Tutorial]
base.subst.H [variable, in AAC_tactics.Tutorial]
base.subst.H' [variable, in AAC_tactics.Tutorial]
_ + _ [notation, in AAC_tactics.Tutorial]
_ * _ [notation, in AAC_tactics.Tutorial]
_ == _ [notation, in AAC_tactics.Tutorial]
0 [notation, in AAC_tactics.Tutorial]
1 [notation, in AAC_tactics.Tutorial]
Bool [module, in AAC_tactics.Instances]
Bool.aac_false [instance, in AAC_tactics.Instances]
Bool.aac_true [instance, in AAC_tactics.Instances]
Bool.aac_andb_Idem [instance, in AAC_tactics.Instances]
Bool.aac_andb_Comm [instance, in AAC_tactics.Instances]
Bool.aac_andb_Assoc [instance, in AAC_tactics.Instances]
Bool.aac_orb_Idem [instance, in AAC_tactics.Instances]
Bool.aac_orb_Comm [instance, in AAC_tactics.Instances]
Bool.aac_orb_Assoc [instance, in AAC_tactics.Instances]
Bool.negb_compat [instance, in AAC_tactics.Instances]
B:12 [binder, in AAC_tactics.Utils]
B:160 [binder, in AAC_tactics.AAC]
B:164 [binder, in AAC_tactics.AAC]
b:17 [binder, in AAC_tactics.Caveats]
b:26 [binder, in AAC_tactics.Caveats]
b:29 [binder, in AAC_tactics.Caveats]
b:34 [binder, in AAC_tactics.Caveats]
b:36 [binder, in AAC_tactics.Caveats]
B:40 [binder, in AAC_tactics.Utils]
b:40 [binder, in AAC_tactics.Caveats]
B:44 [binder, in AAC_tactics.Utils]
B:57 [binder, in AAC_tactics.Utils]
B:77 [binder, in AAC_tactics.Utils]
b:85 [binder, in AAC_tactics.Tutorial]
C
cast [abbreviation, in AAC_tactics.Utils]cast_eq [lemma, in AAC_tactics.Utils]
Caveats [library]
Commutative [record, in AAC_tactics.AAC]
Commutative [inductive, in AAC_tactics.AAC]
Comm:282 [binder, in AAC_tactics.AAC]
compare_weak_spec [inductive, in AAC_tactics.Utils]
compare:78 [binder, in AAC_tactics.Utils]
cons [constructor, in AAC_tactics.Utils]
Constants [library]
c:27 [binder, in AAC_tactics.Caveats]
c:41 [binder, in AAC_tactics.Caveats]
D
decide_false [constructor, in AAC_tactics.Utils]decide_true [constructor, in AAC_tactics.Utils]
decide_spec [inductive, in AAC_tactics.Utils]
dep [section, in AAC_tactics.Utils]
dep.f [variable, in AAC_tactics.Utils]
dep.T [variable, in AAC_tactics.Utils]
dep.U [variable, in AAC_tactics.Utils]
dot_Proper:75 [binder, in AAC_tactics.Caveats]
dot_A:74 [binder, in AAC_tactics.Caveats]
dot_Proper:61 [binder, in AAC_tactics.Caveats]
dot_A:60 [binder, in AAC_tactics.Caveats]
dot_Proper:16 [binder, in AAC_tactics.Tutorial]
dot_A:13 [binder, in AAC_tactics.Tutorial]
dot:10 [binder, in AAC_tactics.Tutorial]
dot:59 [binder, in AAC_tactics.Caveats]
dot:7 [binder, in AAC_tactics.AAC]
dot:73 [binder, in AAC_tactics.Caveats]
E
eq_idx_spec [lemma, in AAC_tactics.Utils]eq_idx_bool [definition, in AAC_tactics.Utils]
eq_subr [lemma, in AAC_tactics.Instances]
evars [section, in AAC_tactics.Caveats]
evars.H [variable, in AAC_tactics.Caveats]
evars.H' [variable, in AAC_tactics.Caveats]
evars.idem [variable, in AAC_tactics.Caveats]
evars.P [variable, in AAC_tactics.Caveats]
Examples [section, in AAC_tactics.Tutorial]
Examples.a [variable, in AAC_tactics.Tutorial]
Examples.b [variable, in AAC_tactics.Tutorial]
Examples.c [variable, in AAC_tactics.Tutorial]
Examples.H [variable, in AAC_tactics.Tutorial]
_ ^2 [notation, in AAC_tactics.Tutorial]
2 ⋅ _ [notation, in AAC_tactics.Tutorial]
E:3 [binder, in AAC_tactics.Caveats]
E:37 [binder, in AAC_tactics.AAC]
E:43 [binder, in AAC_tactics.AAC]
E:49 [binder, in AAC_tactics.AAC]
E:58 [binder, in AAC_tactics.Caveats]
E:72 [binder, in AAC_tactics.Caveats]
E:8 [binder, in AAC_tactics.Tutorial]
E:99 [binder, in AAC_tactics.AAC]
F
fold_map' [definition, in AAC_tactics.Utils]fold_map [definition, in AAC_tactics.Utils]
f:138 [binder, in AAC_tactics.AAC]
f:139 [binder, in AAC_tactics.AAC]
f:334 [binder, in AAC_tactics.AAC]
f:58 [binder, in AAC_tactics.Utils]
G
g:19 [binder, in AAC_tactics.Caveats]H
Hbin1 [lemma, in AAC_tactics.Tutorial]Hbin2 [lemma, in AAC_tactics.Tutorial]
HER:46 [binder, in AAC_tactics.AAC]
HE:44 [binder, in AAC_tactics.AAC]
HE:50 [binder, in AAC_tactics.AAC]
Hnorm:284 [binder, in AAC_tactics.AAC]
Hnorm:327 [binder, in AAC_tactics.AAC]
Hopp [lemma, in AAC_tactics.Tutorial]
HP:31 [binder, in AAC_tactics.Caveats]
HR:359 [binder, in AAC_tactics.AAC]
HR:45 [binder, in AAC_tactics.AAC]
HR:51 [binder, in AAC_tactics.AAC]
HR:54 [binder, in AAC_tactics.AAC]
h1:100 [binder, in AAC_tactics.Utils]
H:146 [binder, in AAC_tactics.AAC]
H:228 [binder, in AAC_tactics.AAC]
H:230 [binder, in AAC_tactics.AAC]
h:258 [binder, in AAC_tactics.AAC]
h:259 [binder, in AAC_tactics.AAC]
H:274 [binder, in AAC_tactics.AAC]
h:285 [binder, in AAC_tactics.AAC]
h:286 [binder, in AAC_tactics.AAC]
h:287 [binder, in AAC_tactics.AAC]
H:3 [binder, in AAC_tactics.Instances]
h:310 [binder, in AAC_tactics.AAC]
h:318 [binder, in AAC_tactics.AAC]
h:328 [binder, in AAC_tactics.AAC]
h:329 [binder, in AAC_tactics.AAC]
h:330 [binder, in AAC_tactics.AAC]
H:344 [binder, in AAC_tactics.AAC]
H:352 [binder, in AAC_tactics.AAC]
H:37 [binder, in AAC_tactics.Utils]
H:46 [binder, in AAC_tactics.Utils]
h:71 [binder, in AAC_tactics.Utils]
H:87 [binder, in AAC_tactics.AAC]
h:88 [binder, in AAC_tactics.Utils]
h:95 [binder, in AAC_tactics.Utils]
I
Idempotent [record, in AAC_tactics.AAC]Idempotent [inductive, in AAC_tactics.AAC]
Idem:289 [binder, in AAC_tactics.AAC]
Idem:293 [binder, in AAC_tactics.AAC]
idx [abbreviation, in AAC_tactics.Utils]
idx_compare_reflect_eq [lemma, in AAC_tactics.Utils]
idx_compare [definition, in AAC_tactics.Utils]
ineq [section, in AAC_tactics.Caveats]
ineq.H [variable, in AAC_tactics.Caveats]
insert [definition, in AAC_tactics.Utils]
insert_aux:104 [binder, in AAC_tactics.Utils]
Instances [library]
Internal [module, in AAC_tactics.AAC]
Internal.add_to_prd [definition, in AAC_tactics.AAC]
Internal.add_to_sum [definition, in AAC_tactics.AAC]
Internal.assoc [instance, in AAC_tactics.AAC]
Internal.Bin [module, in AAC_tactics.AAC]
Internal.Binvalue_Proper [instance, in AAC_tactics.AAC]
Internal.Binvalue_Associative [instance, in AAC_tactics.AAC]
Internal.Binvalue_Idempotent [instance, in AAC_tactics.AAC]
Internal.Binvalue_Commutative [instance, in AAC_tactics.AAC]
Internal.Bin.assoc [projection, in AAC_tactics.AAC]
Internal.Bin.comm [projection, in AAC_tactics.AAC]
Internal.Bin.compat [projection, in AAC_tactics.AAC]
Internal.Bin.idem [projection, in AAC_tactics.AAC]
Internal.Bin.mk_pack [constructor, in AAC_tactics.AAC]
Internal.Bin.pack [record, in AAC_tactics.AAC]
Internal.Bin.t [section, in AAC_tactics.AAC]
Internal.Bin.value [projection, in AAC_tactics.AAC]
Internal.comp [definition, in AAC_tactics.AAC]
Internal.compare [definition, in AAC_tactics.AAC]
Internal.compare_reflect_eq [lemma, in AAC_tactics.AAC]
Internal.compat_prd_Unit [instance, in AAC_tactics.AAC]
Internal.compat_prd_unit_add [lemma, in AAC_tactics.AAC]
Internal.compat_prd_unit_return [lemma, in AAC_tactics.AAC]
Internal.compat_prd_unit [inductive, in AAC_tactics.AAC]
Internal.compat_sum_unit_Unit [instance, in AAC_tactics.AAC]
Internal.compat_sum_unit_add [lemma, in AAC_tactics.AAC]
Internal.compat_sum_unit_return [lemma, in AAC_tactics.AAC]
Internal.compat_sum_unit [inductive, in AAC_tactics.AAC]
Internal.copy [definition, in AAC_tactics.AAC]
Internal.copy [section, in AAC_tactics.AAC]
Internal.copy_idem [lemma, in AAC_tactics.AAC]
Internal.copy_n_unit [lemma, in AAC_tactics.AAC]
Internal.copy_mset_copy [lemma, in AAC_tactics.AAC]
Internal.copy_mset_succ [lemma, in AAC_tactics.AAC]
Internal.copy_mset' [lemma, in AAC_tactics.AAC]
Internal.copy_mset [definition, in AAC_tactics.AAC]
Internal.copy_compat [instance, in AAC_tactics.AAC]
Internal.copy_Psucc [lemma, in AAC_tactics.AAC]
Internal.copy_xH [lemma, in AAC_tactics.AAC]
Internal.copy_plus [lemma, in AAC_tactics.AAC]
Internal.copy' [definition, in AAC_tactics.AAC]
Internal.cpu_right [constructor, in AAC_tactics.AAC]
Internal.cpu_left [constructor, in AAC_tactics.AAC]
Internal.csu_right [constructor, in AAC_tactics.AAC]
Internal.csu_left [constructor, in AAC_tactics.AAC]
Internal.decide [lemma, in AAC_tactics.AAC]
Internal.discr [inductive, in AAC_tactics.AAC]
Internal.eval [definition, in AAC_tactics.AAC]
Internal.eval_norm_aux [definition, in AAC_tactics.AAC]
Internal.eval_norm [definition, in AAC_tactics.AAC]
Internal.eval_norm_lists [lemma, in AAC_tactics.AAC]
Internal.eval_prd_app [lemma, in AAC_tactics.AAC]
Internal.eval_prd_cons [lemma, in AAC_tactics.AAC]
Internal.eval_prd_nil [lemma, in AAC_tactics.AAC]
Internal.eval_reduce_msets [lemma, in AAC_tactics.AAC]
Internal.eval_norm_msets [lemma, in AAC_tactics.AAC]
Internal.eval_merge_bin [lemma, in AAC_tactics.AAC]
Internal.eval_sum_cons [lemma, in AAC_tactics.AAC]
Internal.eval_sum_nil [lemma, in AAC_tactics.AAC]
Internal.eval_aux_compat [instance, in AAC_tactics.AAC]
Internal.eval_aux [definition, in AAC_tactics.AAC]
Internal.is_prd_spec [lemma, in AAC_tactics.AAC]
Internal.is_prd_spec_nothing [constructor, in AAC_tactics.AAC]
Internal.is_prd_spec_unit [constructor, in AAC_tactics.AAC]
Internal.is_prd_spec_op [constructor, in AAC_tactics.AAC]
Internal.is_prd_spec_ind [inductive, in AAC_tactics.AAC]
Internal.is_sum_spec [lemma, in AAC_tactics.AAC]
Internal.is_sum_spec_nothing [constructor, in AAC_tactics.AAC]
Internal.is_sum_spec_unit [constructor, in AAC_tactics.AAC]
Internal.is_sum_spec_op [constructor, in AAC_tactics.AAC]
Internal.is_sum_spec_ind [inductive, in AAC_tactics.AAC]
Internal.is_unit_of_Unit [lemma, in AAC_tactics.AAC]
Internal.is_prd [definition, in AAC_tactics.AAC]
Internal.is_sum [definition, in AAC_tactics.AAC]
Internal.Is_nothing [constructor, in AAC_tactics.AAC]
Internal.Is_unit [constructor, in AAC_tactics.AAC]
Internal.Is_op [constructor, in AAC_tactics.AAC]
Internal.is_idempotent [definition, in AAC_tactics.AAC]
Internal.is_commutative [definition, in AAC_tactics.AAC]
Internal.is_unit_of [definition, in AAC_tactics.AAC]
Internal.left [constructor, in AAC_tactics.AAC]
Internal.lift_normalise [lemma, in AAC_tactics.AAC]
Internal.m [inductive, in AAC_tactics.AAC]
Internal.mk_unit_pack [constructor, in AAC_tactics.AAC]
Internal.mk_unit_for [constructor, in AAC_tactics.AAC]
Internal.norm [definition, in AAC_tactics.AAC]
Internal.normalise [lemma, in AAC_tactics.AAC]
Internal.norm_msets [definition, in AAC_tactics.AAC]
Internal.norm_lists [definition, in AAC_tactics.AAC]
Internal.norm_lists_ [definition, in AAC_tactics.AAC]
Internal.norm_msets_ [definition, in AAC_tactics.AAC]
Internal.prd [constructor, in AAC_tactics.AAC]
Internal.prd' [definition, in AAC_tactics.AAC]
Internal.prd'_prd [lemma, in AAC_tactics.AAC]
Internal.proper [instance, in AAC_tactics.AAC]
Internal.return_prd [definition, in AAC_tactics.AAC]
Internal.return_sum [definition, in AAC_tactics.AAC]
Internal.right [constructor, in AAC_tactics.AAC]
Internal.run_msets [definition, in AAC_tactics.AAC]
Internal.run_list [definition, in AAC_tactics.AAC]
Internal.s [section, in AAC_tactics.AAC]
Internal.sum [constructor, in AAC_tactics.AAC]
Internal.sum' [definition, in AAC_tactics.AAC]
Internal.sum'_sum [lemma, in AAC_tactics.AAC]
Internal.sym [constructor, in AAC_tactics.AAC]
Internal.Sym [module, in AAC_tactics.AAC]
Internal.Sym.ar [projection, in AAC_tactics.AAC]
Internal.Sym.mkPack [constructor, in AAC_tactics.AAC]
Internal.Sym.morph [projection, in AAC_tactics.AAC]
Internal.Sym.null [definition, in AAC_tactics.AAC]
Internal.Sym.pack [record, in AAC_tactics.AAC]
Internal.Sym.rel_of [definition, in AAC_tactics.AAC]
Internal.Sym.t [section, in AAC_tactics.AAC]
Internal.Sym.type_of [definition, in AAC_tactics.AAC]
Internal.Sym.value [projection, in AAC_tactics.AAC]
Internal.s.e_unit [variable, in AAC_tactics.AAC]
Internal.s.e_bin [variable, in AAC_tactics.AAC]
Internal.s.e_sym [variable, in AAC_tactics.AAC]
Internal.s.prds [section, in AAC_tactics.AAC]
Internal.s.prds.i [variable, in AAC_tactics.AAC]
Internal.s.prds.is_unit [variable, in AAC_tactics.AAC]
Internal.s.prd_correctness.is_unit_prd_Unit [variable, in AAC_tactics.AAC]
Internal.s.prd_correctness.is_unit [variable, in AAC_tactics.AAC]
Internal.s.prd_correctness.i [variable, in AAC_tactics.AAC]
Internal.s.prd_correctness [section, in AAC_tactics.AAC]
Internal.s.sums [section, in AAC_tactics.AAC]
Internal.s.sums.i [variable, in AAC_tactics.AAC]
Internal.s.sums.is_unit [variable, in AAC_tactics.AAC]
Internal.s.sum_correctness.comm [variable, in AAC_tactics.AAC]
Internal.s.sum_correctness.is_unit_sum_Unit [variable, in AAC_tactics.AAC]
Internal.s.sum_correctness.is_unit [variable, in AAC_tactics.AAC]
Internal.s.sum_correctness.i [variable, in AAC_tactics.AAC]
Internal.s.sum_correctness [section, in AAC_tactics.AAC]
_ == _ [notation, in AAC_tactics.AAC]
Internal.T [inductive, in AAC_tactics.AAC]
Internal.tcompare_weak_spec [definition, in AAC_tactics.AAC]
Internal.uf_desc [projection, in AAC_tactics.AAC]
Internal.uf_idx [projection, in AAC_tactics.AAC]
Internal.unit [constructor, in AAC_tactics.AAC]
Internal.unit_pack [record, in AAC_tactics.AAC]
Internal.unit_of [record, in AAC_tactics.AAC]
Internal.u_desc [projection, in AAC_tactics.AAC]
Internal.u_value [projection, in AAC_tactics.AAC]
Internal.vcompare [definition, in AAC_tactics.AAC]
Internal.vcompare_reflect_eqdep [definition, in AAC_tactics.AAC]
Internal.vcons [constructor, in AAC_tactics.AAC]
Internal.vnil [constructor, in AAC_tactics.AAC]
Internal.vnorm [definition, in AAC_tactics.AAC]
Internal.vT [inductive, in AAC_tactics.AAC]
Internal.z0 [lemma, in AAC_tactics.AAC]
Internal.z0' [lemma, in AAC_tactics.AAC]
Internal.z1 [lemma, in AAC_tactics.AAC]
Internal.z1' [lemma, in AAC_tactics.AAC]
Internal.z2 [lemma, in AAC_tactics.AAC]
Internal.z2' [lemma, in AAC_tactics.AAC]
introduction [section, in AAC_tactics.Tutorial]
introduction.a [variable, in AAC_tactics.Tutorial]
introduction.b [variable, in AAC_tactics.Tutorial]
introduction.c [variable, in AAC_tactics.Tutorial]
introduction.H [variable, in AAC_tactics.Tutorial]
inv_unique [lemma, in AAC_tactics.Caveats]
is_unit:217 [binder, in AAC_tactics.AAC]
is_unit:211 [binder, in AAC_tactics.AAC]
i:1 [binder, in AAC_tactics.Utils]
i:114 [binder, in AAC_tactics.AAC]
i:118 [binder, in AAC_tactics.AAC]
i:129 [binder, in AAC_tactics.AAC]
i:141 [binder, in AAC_tactics.AAC]
i:149 [binder, in AAC_tactics.AAC]
i:152 [binder, in AAC_tactics.AAC]
i:154 [binder, in AAC_tactics.AAC]
i:155 [binder, in AAC_tactics.AAC]
i:18 [binder, in AAC_tactics.Utils]
i:209 [binder, in AAC_tactics.AAC]
i:215 [binder, in AAC_tactics.AAC]
i:219 [binder, in AAC_tactics.AAC]
i:225 [binder, in AAC_tactics.AAC]
i:227 [binder, in AAC_tactics.AAC]
i:229 [binder, in AAC_tactics.AAC]
i:23 [binder, in AAC_tactics.Utils]
i:231 [binder, in AAC_tactics.AAC]
i:232 [binder, in AAC_tactics.AAC]
i:24 [binder, in AAC_tactics.Utils]
i:26 [binder, in AAC_tactics.Utils]
i:28 [binder, in AAC_tactics.Utils]
i:280 [binder, in AAC_tactics.AAC]
i:288 [binder, in AAC_tactics.AAC]
i:292 [binder, in AAC_tactics.AAC]
i:30 [binder, in AAC_tactics.Utils]
i:325 [binder, in AAC_tactics.AAC]
i:332 [binder, in AAC_tactics.AAC]
i:6 [binder, in AAC_tactics.Utils]
J
j:119 [binder, in AAC_tactics.AAC]j:144 [binder, in AAC_tactics.AAC]
j:151 [binder, in AAC_tactics.AAC]
j:19 [binder, in AAC_tactics.Utils]
j:2 [binder, in AAC_tactics.Utils]
j:226 [binder, in AAC_tactics.AAC]
j:235 [binder, in AAC_tactics.AAC]
j:239 [binder, in AAC_tactics.AAC]
j:241 [binder, in AAC_tactics.AAC]
j:25 [binder, in AAC_tactics.Utils]
j:27 [binder, in AAC_tactics.Utils]
j:270 [binder, in AAC_tactics.AAC]
j:29 [binder, in AAC_tactics.Utils]
j:297 [binder, in AAC_tactics.AAC]
j:301 [binder, in AAC_tactics.AAC]
j:303 [binder, in AAC_tactics.AAC]
j:31 [binder, in AAC_tactics.Utils]
j:7 [binder, in AAC_tactics.Utils]
K
k:18 [binder, in AAC_tactics.Caveats]k:260 [binder, in AAC_tactics.AAC]
k:311 [binder, in AAC_tactics.AAC]
k:72 [binder, in AAC_tactics.Utils]
k:89 [binder, in AAC_tactics.Utils]
k:96 [binder, in AAC_tactics.Utils]
L
law_neutral_right [projection, in AAC_tactics.AAC]law_neutral_left [projection, in AAC_tactics.AAC]
law_idem [projection, in AAC_tactics.AAC]
law_idem [constructor, in AAC_tactics.AAC]
law_comm [projection, in AAC_tactics.AAC]
law_comm [constructor, in AAC_tactics.AAC]
law_assoc [projection, in AAC_tactics.AAC]
law_assoc [constructor, in AAC_tactics.AAC]
lex [abbreviation, in AAC_tactics.Utils]
lift_reflexivity [lemma, in AAC_tactics.AAC]
lift_transitivity_right [lemma, in AAC_tactics.AAC]
lift_transitivity_left [lemma, in AAC_tactics.AAC]
lift_le_eq [instance, in AAC_tactics.Tutorial]
lists [section, in AAC_tactics.Utils]
Lists [module, in AAC_tactics.Instances]
Lists [section, in AAC_tactics.Tutorial]
Lists.aac_nil_Permutation_append [instance, in AAC_tactics.Instances]
Lists.aac_append_Permutation_Comm [instance, in AAC_tactics.Instances]
Lists.aac_append_Permutation_Assoc [instance, in AAC_tactics.Instances]
Lists.aac_append_Proper [instance, in AAC_tactics.Instances]
Lists.aac_nil_append [instance, in AAC_tactics.Instances]
Lists.aac_append_Assoc [instance, in AAC_tactics.Instances]
lists.c [section, in AAC_tactics.Utils]
lists.c.A [variable, in AAC_tactics.Utils]
lists.c.B [variable, in AAC_tactics.Utils]
lists.c.compare [variable, in AAC_tactics.Utils]
Lists.H [variable, in AAC_tactics.Tutorial]
lists.list_compare_weak_spec.Hcompare [variable, in AAC_tactics.Utils]
lists.list_compare_weak_spec.compare [variable, in AAC_tactics.Utils]
lists.list_compare_weak_spec.A [variable, in AAC_tactics.Utils]
lists.list_compare_weak_spec [section, in AAC_tactics.Utils]
Lists.l1 [variable, in AAC_tactics.Tutorial]
Lists.l2 [variable, in AAC_tactics.Tutorial]
Lists.l3 [variable, in AAC_tactics.Tutorial]
lists.m [section, in AAC_tactics.Utils]
lists.mset_compare_weak_spec.Hcompare [variable, in AAC_tactics.Utils]
lists.mset_compare_weak_spec.compare [variable, in AAC_tactics.Utils]
lists.mset_compare_weak_spec.A [variable, in AAC_tactics.Utils]
lists.mset_compare_weak_spec [section, in AAC_tactics.Utils]
lists.m.A [variable, in AAC_tactics.Utils]
lists.m.B [variable, in AAC_tactics.Utils]
lists.m.bind [variable, in AAC_tactics.Utils]
lists.m.b2 [variable, in AAC_tactics.Utils]
lists.m.compare [variable, in AAC_tactics.Utils]
lists.m.map [variable, in AAC_tactics.Utils]
lists.m.merge [variable, in AAC_tactics.Utils]
lists.m.ret [variable, in AAC_tactics.Utils]
Lists.X [variable, in AAC_tactics.Tutorial]
list_compare_weak_spec [lemma, in AAC_tactics.Utils]
list_compare [definition, in AAC_tactics.Utils]
l':167 [binder, in AAC_tactics.AAC]
l':64 [binder, in AAC_tactics.Utils]
l1:105 [binder, in AAC_tactics.Utils]
l2:101 [binder, in AAC_tactics.Utils]
l2:108 [binder, in AAC_tactics.Utils]
l2:109 [binder, in AAC_tactics.Utils]
l:11 [binder, in AAC_tactics.Instances]
l:117 [binder, in AAC_tactics.Utils]
l:121 [binder, in AAC_tactics.Utils]
l:126 [binder, in AAC_tactics.Utils]
l:150 [binder, in AAC_tactics.AAC]
l:166 [binder, in AAC_tactics.AAC]
l:176 [binder, in AAC_tactics.AAC]
l:184 [binder, in AAC_tactics.AAC]
l:186 [binder, in AAC_tactics.AAC]
l:188 [binder, in AAC_tactics.AAC]
l:200 [binder, in AAC_tactics.AAC]
l:202 [binder, in AAC_tactics.AAC]
l:204 [binder, in AAC_tactics.AAC]
l:210 [binder, in AAC_tactics.AAC]
l:216 [binder, in AAC_tactics.AAC]
l:220 [binder, in AAC_tactics.AAC]
l:240 [binder, in AAC_tactics.AAC]
l:245 [binder, in AAC_tactics.AAC]
l:249 [binder, in AAC_tactics.AAC]
l:262 [binder, in AAC_tactics.AAC]
l:266 [binder, in AAC_tactics.AAC]
l:272 [binder, in AAC_tactics.AAC]
l:302 [binder, in AAC_tactics.AAC]
l:306 [binder, in AAC_tactics.AAC]
l:309 [binder, in AAC_tactics.AAC]
l:320 [binder, in AAC_tactics.AAC]
l:333 [binder, in AAC_tactics.AAC]
l:59 [binder, in AAC_tactics.Utils]
l:63 [binder, in AAC_tactics.Utils]
M
map:3 [binder, in AAC_tactics.AAC]merge_map [definition, in AAC_tactics.Utils]
merge_aux:112 [binder, in AAC_tactics.Utils]
merge_msets [definition, in AAC_tactics.Utils]
merge:165 [binder, in AAC_tactics.AAC]
morphism [section, in AAC_tactics.Caveats]
morphism.H [variable, in AAC_tactics.Caveats]
mset [definition, in AAC_tactics.Utils]
mset_compare_weak_spec [lemma, in AAC_tactics.Utils]
mset_compare [definition, in AAC_tactics.Utils]
m:253 [binder, in AAC_tactics.AAC]
m:268 [binder, in AAC_tactics.AAC]
m:294 [binder, in AAC_tactics.AAC]
m:315 [binder, in AAC_tactics.AAC]
m:69 [binder, in AAC_tactics.AAC]
N
N [module, in AAC_tactics.Instances]nelist [inductive, in AAC_tactics.Utils]
nelist_map [definition, in AAC_tactics.Utils]
nil [constructor, in AAC_tactics.Utils]
norm:185 [binder, in AAC_tactics.AAC]
norm:201 [binder, in AAC_tactics.AAC]
norm:208 [binder, in AAC_tactics.AAC]
norm:214 [binder, in AAC_tactics.AAC]
norm:281 [binder, in AAC_tactics.AAC]
null:2 [binder, in AAC_tactics.AAC]
N.aac_zero_max [instance, in AAC_tactics.Instances]
N.aac_zero [instance, in AAC_tactics.Instances]
N.aac_one [instance, in AAC_tactics.Instances]
N.aac_Nmax_Idem [instance, in AAC_tactics.Instances]
N.aac_Nmax_Assoc [instance, in AAC_tactics.Instances]
N.aac_Nmax_Comm [instance, in AAC_tactics.Instances]
N.aac_Nmin_Idem [instance, in AAC_tactics.Instances]
N.aac_Nmin_Assoc [instance, in AAC_tactics.Instances]
N.aac_Nmin_Comm [instance, in AAC_tactics.Instances]
N.aac_Nmult_Assoc [instance, in AAC_tactics.Instances]
N.aac_Nmult_Comm [instance, in AAC_tactics.Instances]
N.aac_Nplus_Comm [instance, in AAC_tactics.Instances]
N.aac_Nplus_Assoc [instance, in AAC_tactics.Instances]
N.lift_le_eq [instance, in AAC_tactics.Instances]
N.preorder_le [instance, in AAC_tactics.Instances]
n1:99 [binder, in AAC_tactics.Utils]
n:11 [binder, in AAC_tactics.Caveats]
n:115 [binder, in AAC_tactics.AAC]
n:14 [binder, in AAC_tactics.Caveats]
n:175 [binder, in AAC_tactics.AAC]
n:181 [binder, in AAC_tactics.AAC]
n:183 [binder, in AAC_tactics.AAC]
n:247 [binder, in AAC_tactics.AAC]
n:255 [binder, in AAC_tactics.AAC]
n:257 [binder, in AAC_tactics.AAC]
n:261 [binder, in AAC_tactics.AAC]
n:265 [binder, in AAC_tactics.AAC]
n:267 [binder, in AAC_tactics.AAC]
n:271 [binder, in AAC_tactics.AAC]
n:275 [binder, in AAC_tactics.AAC]
n:278 [binder, in AAC_tactics.AAC]
n:290 [binder, in AAC_tactics.AAC]
n:4 [binder, in AAC_tactics.AAC]
n:59 [binder, in AAC_tactics.AAC]
n:65 [binder, in AAC_tactics.AAC]
n:68 [binder, in AAC_tactics.AAC]
n:72 [binder, in AAC_tactics.AAC]
n:74 [binder, in AAC_tactics.AAC]
n:77 [binder, in AAC_tactics.AAC]
n:80 [binder, in AAC_tactics.AAC]
O
one:12 [binder, in AAC_tactics.Tutorial]One:19 [binder, in AAC_tactics.Tutorial]
one:62 [binder, in AAC_tactics.Caveats]
One:63 [binder, in AAC_tactics.Caveats]
one:76 [binder, in AAC_tactics.Caveats]
One:77 [binder, in AAC_tactics.Caveats]
op':57 [binder, in AAC_tactics.AAC]
op:28 [binder, in AAC_tactics.AAC]
op:56 [binder, in AAC_tactics.AAC]
o:134 [binder, in AAC_tactics.AAC]
P
P [module, in AAC_tactics.Instances]parameters [section, in AAC_tactics.Caveats]
parameters.f [variable, in AAC_tactics.Caveats]
parameters.g [variable, in AAC_tactics.Caveats]
parameters.H [variable, in AAC_tactics.Caveats]
parameters.Hf [variable, in AAC_tactics.Caveats]
parameters.Hf' [variable, in AAC_tactics.Caveats]
parameters.Hg [variable, in AAC_tactics.Caveats]
_ + _ [notation, in AAC_tactics.Caveats]
_ == _ [notation, in AAC_tactics.Caveats]
0 [notation, in AAC_tactics.Caveats]
pcws_gt [constructor, in AAC_tactics.Utils]
pcws_lt [constructor, in AAC_tactics.Utils]
pcws_eq [constructor, in AAC_tactics.Utils]
Peano [section, in AAC_tactics.Caveats]
Peano [module, in AAC_tactics.Instances]
Peano [section, in AAC_tactics.Tutorial]
Peano.a [variable, in AAC_tactics.Tutorial]
Peano.aac_zero_max [instance, in AAC_tactics.Instances]
Peano.aac_zero_add [instance, in AAC_tactics.Instances]
Peano.aac_one [instance, in AAC_tactics.Instances]
Peano.aac_max_Idem [instance, in AAC_tactics.Instances]
Peano.aac_max_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_max_Comm [instance, in AAC_tactics.Instances]
Peano.aac_min_Idem [instance, in AAC_tactics.Instances]
Peano.aac_min_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_min_Comm [instance, in AAC_tactics.Instances]
Peano.aac_mul_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_mul_Comm [instance, in AAC_tactics.Instances]
Peano.aac_add_Comm [instance, in AAC_tactics.Instances]
Peano.aac_add_Assoc [instance, in AAC_tactics.Instances]
Peano.b [variable, in AAC_tactics.Tutorial]
Peano.c [variable, in AAC_tactics.Tutorial]
Peano.H [variable, in AAC_tactics.Caveats]
Peano.H [variable, in AAC_tactics.Tutorial]
Peano.H' [variable, in AAC_tactics.Caveats]
Peano.lift_le_eq [instance, in AAC_tactics.Instances]
Peano.preorder_le [instance, in AAC_tactics.Instances]
plus_Proper:7 [binder, in AAC_tactics.Caveats]
plus_C:6 [binder, in AAC_tactics.Caveats]
plus_A:5 [binder, in AAC_tactics.Caveats]
plus_Proper:17 [binder, in AAC_tactics.Tutorial]
plus_C:15 [binder, in AAC_tactics.Tutorial]
plus_A:14 [binder, in AAC_tactics.Tutorial]
plus:15 [binder, in AAC_tactics.AAC]
plus:22 [binder, in AAC_tactics.AAC]
plus:4 [binder, in AAC_tactics.Caveats]
plus:55 [binder, in AAC_tactics.AAC]
plus:9 [binder, in AAC_tactics.Tutorial]
pos_compare_weak_spec [lemma, in AAC_tactics.Utils]
pos_compare [abbreviation, in AAC_tactics.Utils]
po:58 [binder, in AAC_tactics.AAC]
Proper_Zplus [instance, in AAC_tactics.Tutorial]
Prop_ops.lift_impl_iff [instance, in AAC_tactics.Instances]
Prop_ops.aac_not_compat [instance, in AAC_tactics.Instances]
Prop_ops.aac_False [instance, in AAC_tactics.Instances]
Prop_ops.aac_True [instance, in AAC_tactics.Instances]
Prop_ops.aac_and_Idem [instance, in AAC_tactics.Instances]
Prop_ops.aac_or_Idem [instance, in AAC_tactics.Instances]
Prop_ops.aac_or_Comm [instance, in AAC_tactics.Instances]
Prop_ops.aac_or_Assoc [instance, in AAC_tactics.Instances]
Prop_ops [module, in AAC_tactics.Instances]
P.aac_one_max [instance, in AAC_tactics.Instances]
P.aac_one [instance, in AAC_tactics.Instances]
P.aac_Pmax_Idem [instance, in AAC_tactics.Instances]
P.aac_Pmax_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pmax_Comm [instance, in AAC_tactics.Instances]
P.aac_Pmin_Idem [instance, in AAC_tactics.Instances]
P.aac_Pmin_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pmin_Comm [instance, in AAC_tactics.Instances]
P.aac_Pmult_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pmult_Comm [instance, in AAC_tactics.Instances]
P.aac_Pplus_Comm [instance, in AAC_tactics.Instances]
P.aac_Pplus_Assoc [instance, in AAC_tactics.Instances]
P.lift_le_eq [instance, in AAC_tactics.Instances]
P.Pmult_1_l [lemma, in AAC_tactics.Instances]
P.preorder_le [instance, in AAC_tactics.Instances]
p:153 [binder, in AAC_tactics.AAC]
p:269 [binder, in AAC_tactics.AAC]
P:30 [binder, in AAC_tactics.Caveats]
p:319 [binder, in AAC_tactics.AAC]
Q
Q [module, in AAC_tactics.Instances]Q.aac_zero_Qplus [instance, in AAC_tactics.Instances]
Q.aac_one [instance, in AAC_tactics.Instances]
Q.aac_Qmax_Idem [instance, in AAC_tactics.Instances]
Q.aac_Qmax_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Qmax_Comm [instance, in AAC_tactics.Instances]
Q.aac_Qmin_Idem [instance, in AAC_tactics.Instances]
Q.aac_Qmin_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Qmin_Comm [instance, in AAC_tactics.Instances]
Q.aac_Qmult_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Qmult_Comm [instance, in AAC_tactics.Instances]
Q.aac_Qplus_Comm [instance, in AAC_tactics.Instances]
Q.aac_Qplus_Assoc [instance, in AAC_tactics.Instances]
Q.lift_le_eq [instance, in AAC_tactics.Instances]
Q.preorder_le [instance, in AAC_tactics.Instances]
R
reduce_mset [definition, in AAC_tactics.Utils]reflect_eqdep_weak_spec [lemma, in AAC_tactics.Utils]
reflect_eqdep_eq [lemma, in AAC_tactics.Utils]
reflect_eqdep [definition, in AAC_tactics.Utils]
Relations [module, in AAC_tactics.Instances]
Relations.aac_eq [instance, in AAC_tactics.Instances]
Relations.aac_compo [instance, in AAC_tactics.Instances]
Relations.aac_top [instance, in AAC_tactics.Instances]
Relations.aac_inter_Idem [instance, in AAC_tactics.Instances]
Relations.aac_inter_Assoc [instance, in AAC_tactics.Instances]
Relations.aac_inter_Comm [instance, in AAC_tactics.Instances]
Relations.aac_bot [instance, in AAC_tactics.Instances]
Relations.aac_union_Idem [instance, in AAC_tactics.Instances]
Relations.aac_union_Assoc [instance, in AAC_tactics.Instances]
Relations.aac_union_Comm [instance, in AAC_tactics.Instances]
Relations.bot [definition, in AAC_tactics.Instances]
Relations.clos_refl_trans_compat [instance, in AAC_tactics.Instances]
Relations.clos_refl_trans_incr [instance, in AAC_tactics.Instances]
Relations.clos_trans_compat [instance, in AAC_tactics.Instances]
Relations.clos_trans_incr [instance, in AAC_tactics.Instances]
Relations.compo [definition, in AAC_tactics.Instances]
Relations.defs [section, in AAC_tactics.Instances]
Relations.defs.R [variable, in AAC_tactics.Instances]
Relations.defs.S [variable, in AAC_tactics.Instances]
Relations.defs.T [variable, in AAC_tactics.Instances]
Relations.eq_same_relation [instance, in AAC_tactics.Instances]
Relations.inter [definition, in AAC_tactics.Instances]
Relations.lift_inclusion_same_relation [instance, in AAC_tactics.Instances]
Relations.negr [definition, in AAC_tactics.Instances]
Relations.negr_compat [instance, in AAC_tactics.Instances]
Relations.preorder_inclusion [instance, in AAC_tactics.Instances]
Relations.top [definition, in AAC_tactics.Instances]
Relations.transp_compat [instance, in AAC_tactics.Instances]
R:13 [binder, in AAC_tactics.Utils]
R:14 [binder, in AAC_tactics.AAC]
R:2 [binder, in AAC_tactics.Caveats]
R:2 [binder, in AAC_tactics.Instances]
R:21 [binder, in AAC_tactics.AAC]
R:27 [binder, in AAC_tactics.AAC]
r:273 [binder, in AAC_tactics.AAC]
r:321 [binder, in AAC_tactics.AAC]
R:36 [binder, in AAC_tactics.AAC]
R:42 [binder, in AAC_tactics.AAC]
R:48 [binder, in AAC_tactics.AAC]
R:53 [binder, in AAC_tactics.AAC]
R:57 [binder, in AAC_tactics.Caveats]
R:6 [binder, in AAC_tactics.AAC]
R:7 [binder, in AAC_tactics.Tutorial]
R:71 [binder, in AAC_tactics.Caveats]
R:76 [binder, in AAC_tactics.AAC]
R:90 [binder, in AAC_tactics.AAC]
R:98 [binder, in AAC_tactics.AAC]
S
sigma [definition, in AAC_tactics.AAC]sigma [section, in AAC_tactics.AAC]
sigma_empty [definition, in AAC_tactics.AAC]
sigma_add [definition, in AAC_tactics.AAC]
sigma_get [definition, in AAC_tactics.AAC]
S:343 [binder, in AAC_tactics.AAC]
T
t [section, in AAC_tactics.AAC]Tutorial [library]
T:24 [binder, in AAC_tactics.Instances]
T:25 [binder, in AAC_tactics.Instances]
T:26 [binder, in AAC_tactics.Instances]
T:27 [binder, in AAC_tactics.Instances]
T:28 [binder, in AAC_tactics.Instances]
T:29 [binder, in AAC_tactics.Instances]
T:30 [binder, in AAC_tactics.Instances]
T:31 [binder, in AAC_tactics.Instances]
T:32 [binder, in AAC_tactics.Instances]
T:33 [binder, in AAC_tactics.Instances]
T:34 [binder, in AAC_tactics.Instances]
T:35 [binder, in AAC_tactics.Instances]
T:36 [binder, in AAC_tactics.Instances]
T:37 [binder, in AAC_tactics.Instances]
T:38 [binder, in AAC_tactics.Instances]
T:39 [binder, in AAC_tactics.Instances]
T:40 [binder, in AAC_tactics.Instances]
T:41 [binder, in AAC_tactics.Instances]
T:42 [binder, in AAC_tactics.Instances]
U
U [section, in AAC_tactics.Caveats]Unit [record, in AAC_tactics.AAC]
unit:29 [binder, in AAC_tactics.AAC]
Unnamed_thm5 [definition, in AAC_tactics.Caveats]
Unnamed_thm5 [definition, in AAC_tactics.Caveats]
Unnamed_thm5 [definition, in AAC_tactics.Caveats]
Unnamed_thm5 [definition, in AAC_tactics.Caveats]
Unnamed_thm4 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm3 [definition, in AAC_tactics.Caveats]
Unnamed_thm2 [definition, in AAC_tactics.Caveats]
Unnamed_thm1 [definition, in AAC_tactics.Caveats]
Unnamed_thm1 [definition, in AAC_tactics.Caveats]
Unnamed_thm0 [definition, in AAC_tactics.Caveats]
Unnamed_thm [definition, in AAC_tactics.Caveats]
Unnamed_thm24 [definition, in AAC_tactics.Tutorial]
Unnamed_thm23 [definition, in AAC_tactics.Tutorial]
Unnamed_thm22 [definition, in AAC_tactics.Tutorial]
Unnamed_thm21 [definition, in AAC_tactics.Tutorial]
Unnamed_thm20 [definition, in AAC_tactics.Tutorial]
Unnamed_thm20 [definition, in AAC_tactics.Tutorial]
Unnamed_thm20 [definition, in AAC_tactics.Tutorial]
Unnamed_thm19 [definition, in AAC_tactics.Tutorial]
Unnamed_thm18 [definition, in AAC_tactics.Tutorial]
Unnamed_thm17 [definition, in AAC_tactics.Tutorial]
Unnamed_thm16 [definition, in AAC_tactics.Tutorial]
Unnamed_thm15 [definition, in AAC_tactics.Tutorial]
Unnamed_thm14 [definition, in AAC_tactics.Tutorial]
Unnamed_thm13 [definition, in AAC_tactics.Tutorial]
Unnamed_thm12 [definition, in AAC_tactics.Tutorial]
Unnamed_thm11 [definition, in AAC_tactics.Tutorial]
Unnamed_thm11 [definition, in AAC_tactics.Tutorial]
Unnamed_thm10 [definition, in AAC_tactics.Tutorial]
Unnamed_thm9 [definition, in AAC_tactics.Tutorial]
Unnamed_thm8 [definition, in AAC_tactics.Tutorial]
Unnamed_thm7 [definition, in AAC_tactics.Tutorial]
Unnamed_thm6 [definition, in AAC_tactics.Tutorial]
Unnamed_thm5 [definition, in AAC_tactics.Tutorial]
Unnamed_thm4 [definition, in AAC_tactics.Tutorial]
Unnamed_thm3 [definition, in AAC_tactics.Tutorial]
Unnamed_thm2 [definition, in AAC_tactics.Tutorial]
Unnamed_thm1 [definition, in AAC_tactics.Tutorial]
Unnamed_thm0 [definition, in AAC_tactics.Tutorial]
Unnamed_thm [definition, in AAC_tactics.Tutorial]
un:135 [binder, in AAC_tactics.AAC]
un:187 [binder, in AAC_tactics.AAC]
un:190 [binder, in AAC_tactics.AAC]
un:79 [binder, in AAC_tactics.Utils]
us:120 [binder, in AAC_tactics.AAC]
us:142 [binder, in AAC_tactics.AAC]
Utils [library]
U.dot_inv_right [variable, in AAC_tactics.Caveats]
U.dot_inv_left [variable, in AAC_tactics.Caveats]
U.f [variable, in AAC_tactics.Caveats]
U.Hf [variable, in AAC_tactics.Caveats]
_ * _ [notation, in AAC_tactics.Caveats]
_ == _ [notation, in AAC_tactics.Caveats]
1 [notation, in AAC_tactics.Caveats]
u:102 [binder, in AAC_tactics.AAC]
u:116 [binder, in AAC_tactics.AAC]
u:128 [binder, in AAC_tactics.AAC]
u:140 [binder, in AAC_tactics.AAC]
u:171 [binder, in AAC_tactics.AAC]
u:173 [binder, in AAC_tactics.AAC]
u:180 [binder, in AAC_tactics.AAC]
u:182 [binder, in AAC_tactics.AAC]
u:194 [binder, in AAC_tactics.AAC]
u:196 [binder, in AAC_tactics.AAC]
u:198 [binder, in AAC_tactics.AAC]
u:199 [binder, in AAC_tactics.AAC]
u:203 [binder, in AAC_tactics.AAC]
u:205 [binder, in AAC_tactics.AAC]
u:218 [binder, in AAC_tactics.AAC]
u:242 [binder, in AAC_tactics.AAC]
u:243 [binder, in AAC_tactics.AAC]
u:277 [binder, in AAC_tactics.AAC]
u:283 [binder, in AAC_tactics.AAC]
u:304 [binder, in AAC_tactics.AAC]
u:305 [binder, in AAC_tactics.AAC]
u:323 [binder, in AAC_tactics.AAC]
u:326 [binder, in AAC_tactics.AAC]
u:331 [binder, in AAC_tactics.AAC]
u:337 [binder, in AAC_tactics.AAC]
u:339 [binder, in AAC_tactics.AAC]
u:34 [binder, in AAC_tactics.Utils]
u:341 [binder, in AAC_tactics.AAC]
u:345 [binder, in AAC_tactics.AAC]
u:38 [binder, in AAC_tactics.Utils]
u:43 [binder, in AAC_tactics.Utils]
u:48 [binder, in AAC_tactics.Utils]
u:51 [binder, in AAC_tactics.Utils]
u:85 [binder, in AAC_tactics.Utils]
u:92 [binder, in AAC_tactics.Utils]
V
V [section, in AAC_tactics.Caveats]vm:178 [binder, in AAC_tactics.AAC]
vm:263 [binder, in AAC_tactics.AAC]
vm:80 [binder, in AAC_tactics.Utils]
vs:121 [binder, in AAC_tactics.AAC]
vs:145 [binder, in AAC_tactics.AAC]
_ * _ [notation, in AAC_tactics.Caveats]
_ == _ [notation, in AAC_tactics.Caveats]
1 [notation, in AAC_tactics.Caveats]
v:117 [binder, in AAC_tactics.AAC]
v:130 [binder, in AAC_tactics.AAC]
v:143 [binder, in AAC_tactics.AAC]
v:338 [binder, in AAC_tactics.AAC]
v:340 [binder, in AAC_tactics.AAC]
v:342 [binder, in AAC_tactics.AAC]
v:346 [binder, in AAC_tactics.AAC]
v:35 [binder, in AAC_tactics.Utils]
v:45 [binder, in AAC_tactics.Utils]
v:49 [binder, in AAC_tactics.Utils]
v:52 [binder, in AAC_tactics.Utils]
v:86 [binder, in AAC_tactics.Utils]
v:93 [binder, in AAC_tactics.Utils]
W
W [section, in AAC_tactics.Caveats]W.a [variable, in AAC_tactics.Caveats]
W.b [variable, in AAC_tactics.Caveats]
W.c [variable, in AAC_tactics.Caveats]
W.H [variable, in AAC_tactics.Caveats]
X
xn:63 [binder, in AAC_tactics.AAC]xn:64 [binder, in AAC_tactics.AAC]
xn:67 [binder, in AAC_tactics.AAC]
X:1 [binder, in AAC_tactics.Caveats]
X:1 [binder, in AAC_tactics.Instances]
x:10 [binder, in AAC_tactics.Instances]
x:113 [binder, in AAC_tactics.Utils]
x:12 [binder, in AAC_tactics.Caveats]
x:12 [binder, in AAC_tactics.Instances]
X:13 [binder, in AAC_tactics.AAC]
x:13 [binder, in AAC_tactics.Instances]
x:14 [binder, in AAC_tactics.Utils]
x:17 [binder, in AAC_tactics.AAC]
x:17 [binder, in AAC_tactics.Instances]
x:19 [binder, in AAC_tactics.Instances]
X:20 [binder, in AAC_tactics.AAC]
x:20 [binder, in AAC_tactics.Caveats]
x:20 [binder, in AAC_tactics.Tutorial]
x:206 [binder, in AAC_tactics.AAC]
x:212 [binder, in AAC_tactics.AAC]
x:22 [binder, in AAC_tactics.Instances]
x:24 [binder, in AAC_tactics.AAC]
x:246 [binder, in AAC_tactics.AAC]
x:252 [binder, in AAC_tactics.AAC]
x:254 [binder, in AAC_tactics.AAC]
x:256 [binder, in AAC_tactics.AAC]
X:26 [binder, in AAC_tactics.AAC]
x:276 [binder, in AAC_tactics.AAC]
x:279 [binder, in AAC_tactics.AAC]
x:291 [binder, in AAC_tactics.AAC]
x:307 [binder, in AAC_tactics.AAC]
x:31 [binder, in AAC_tactics.AAC]
x:31 [binder, in AAC_tactics.Tutorial]
x:314 [binder, in AAC_tactics.AAC]
x:316 [binder, in AAC_tactics.AAC]
x:317 [binder, in AAC_tactics.AAC]
x:324 [binder, in AAC_tactics.AAC]
x:33 [binder, in AAC_tactics.AAC]
x:347 [binder, in AAC_tactics.AAC]
X:35 [binder, in AAC_tactics.AAC]
x:354 [binder, in AAC_tactics.AAC]
x:357 [binder, in AAC_tactics.AAC]
x:360 [binder, in AAC_tactics.AAC]
x:37 [binder, in AAC_tactics.Caveats]
x:37 [binder, in AAC_tactics.Tutorial]
x:4 [binder, in AAC_tactics.Tutorial]
X:41 [binder, in AAC_tactics.AAC]
x:42 [binder, in AAC_tactics.Caveats]
x:43 [binder, in AAC_tactics.Tutorial]
x:44 [binder, in AAC_tactics.Caveats]
x:46 [binder, in AAC_tactics.Tutorial]
X:47 [binder, in AAC_tactics.AAC]
x:49 [binder, in AAC_tactics.Caveats]
X:5 [binder, in AAC_tactics.AAC]
X:52 [binder, in AAC_tactics.AAC]
x:52 [binder, in AAC_tactics.Caveats]
x:52 [binder, in AAC_tactics.Tutorial]
x:54 [binder, in AAC_tactics.Caveats]
x:55 [binder, in AAC_tactics.Tutorial]
X:56 [binder, in AAC_tactics.Caveats]
X:6 [binder, in AAC_tactics.Tutorial]
x:60 [binder, in AAC_tactics.AAC]
x:60 [binder, in AAC_tactics.Tutorial]
x:62 [binder, in AAC_tactics.Tutorial]
x:66 [binder, in AAC_tactics.AAC]
x:66 [binder, in AAC_tactics.Caveats]
x:68 [binder, in AAC_tactics.Caveats]
x:69 [binder, in AAC_tactics.Tutorial]
x:70 [binder, in AAC_tactics.AAC]
X:70 [binder, in AAC_tactics.Caveats]
x:71 [binder, in AAC_tactics.AAC]
x:73 [binder, in AAC_tactics.AAC]
x:73 [binder, in AAC_tactics.Tutorial]
x:74 [binder, in AAC_tactics.Tutorial]
X:75 [binder, in AAC_tactics.AAC]
x:75 [binder, in AAC_tactics.Tutorial]
x:76 [binder, in AAC_tactics.Tutorial]
x:78 [binder, in AAC_tactics.Caveats]
x:81 [binder, in AAC_tactics.Tutorial]
x:83 [binder, in AAC_tactics.Tutorial]
x:86 [binder, in AAC_tactics.Tutorial]
x:88 [binder, in AAC_tactics.AAC]
x:88 [binder, in AAC_tactics.Tutorial]
X:89 [binder, in AAC_tactics.AAC]
x:89 [binder, in AAC_tactics.Caveats]
x:9 [binder, in AAC_tactics.AAC]
x:90 [binder, in AAC_tactics.Tutorial]
x:91 [binder, in AAC_tactics.Caveats]
x:93 [binder, in AAC_tactics.Caveats]
X:97 [binder, in AAC_tactics.AAC]
Y
y':80 [binder, in AAC_tactics.Caveats]y:10 [binder, in AAC_tactics.AAC]
y:15 [binder, in AAC_tactics.Utils]
y:18 [binder, in AAC_tactics.AAC]
y:18 [binder, in AAC_tactics.Instances]
y:20 [binder, in AAC_tactics.Instances]
y:21 [binder, in AAC_tactics.Caveats]
y:23 [binder, in AAC_tactics.Instances]
y:32 [binder, in AAC_tactics.Tutorial]
y:348 [binder, in AAC_tactics.AAC]
y:353 [binder, in AAC_tactics.AAC]
y:356 [binder, in AAC_tactics.AAC]
y:361 [binder, in AAC_tactics.AAC]
y:44 [binder, in AAC_tactics.Tutorial]
y:50 [binder, in AAC_tactics.Caveats]
y:53 [binder, in AAC_tactics.Tutorial]
y:63 [binder, in AAC_tactics.Tutorial]
y:70 [binder, in AAC_tactics.Tutorial]
y:79 [binder, in AAC_tactics.Caveats]
y:82 [binder, in AAC_tactics.Tutorial]
y:87 [binder, in AAC_tactics.Tutorial]
y:89 [binder, in AAC_tactics.Tutorial]
y:94 [binder, in AAC_tactics.Caveats]
Z
Z [section, in AAC_tactics.Caveats]Z [module, in AAC_tactics.Instances]
Zabs_triangle [lemma, in AAC_tactics.Tutorial]
zero:11 [binder, in AAC_tactics.Tutorial]
Zero:18 [binder, in AAC_tactics.Tutorial]
zero:8 [binder, in AAC_tactics.Caveats]
Zero:9 [binder, in AAC_tactics.Caveats]
Zminus_compat [instance, in AAC_tactics.Tutorial]
Zplus_incr [instance, in AAC_tactics.Caveats]
Zplus_opp_r [lemma, in AAC_tactics.Tutorial]
Z.a [variable, in AAC_tactics.Caveats]
Z.aac_zero_Zplus [instance, in AAC_tactics.Instances]
Z.aac_one [instance, in AAC_tactics.Instances]
Z.aac_Zmax_Idem [instance, in AAC_tactics.Instances]
Z.aac_Zmax_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Zmax_Comm [instance, in AAC_tactics.Instances]
Z.aac_Zmin_Idem [instance, in AAC_tactics.Instances]
Z.aac_Zmin_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Zmin_Comm [instance, in AAC_tactics.Instances]
Z.aac_Zmult_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Zmult_Comm [instance, in AAC_tactics.Instances]
Z.aac_Zplus_Comm [instance, in AAC_tactics.Instances]
Z.aac_Zplus_Assoc [instance, in AAC_tactics.Instances]
Z.b [variable, in AAC_tactics.Caveats]
Z.c [variable, in AAC_tactics.Caveats]
Z.f [variable, in AAC_tactics.Caveats]
Z.H [variable, in AAC_tactics.Caveats]
Z.H0 [variable, in AAC_tactics.Caveats]
Z.H1 [variable, in AAC_tactics.Caveats]
Z.lift_le_eq [instance, in AAC_tactics.Instances]
Z.preorder_Zle [instance, in AAC_tactics.Instances]
z:11 [binder, in AAC_tactics.AAC]
z:21 [binder, in AAC_tactics.Instances]
z:355 [binder, in AAC_tactics.AAC]
z:358 [binder, in AAC_tactics.AAC]
z:64 [binder, in AAC_tactics.Tutorial]
z:71 [binder, in AAC_tactics.Tutorial]
other
_ ++ _ [notation, in AAC_tactics.Utils]_ :: _ [notation, in AAC_tactics.Utils]
Notation Index
B
_ + _ [in AAC_tactics.Tutorial]_ * _ [in AAC_tactics.Tutorial]
_ == _ [in AAC_tactics.Tutorial]
0 [in AAC_tactics.Tutorial]
1 [in AAC_tactics.Tutorial]
E
_ ^2 [in AAC_tactics.Tutorial]2 ⋅ _ [in AAC_tactics.Tutorial]
I
_ == _ [in AAC_tactics.AAC]P
_ + _ [in AAC_tactics.Caveats]_ == _ [in AAC_tactics.Caveats]
0 [in AAC_tactics.Caveats]
U
_ * _ [in AAC_tactics.Caveats]_ == _ [in AAC_tactics.Caveats]
1 [in AAC_tactics.Caveats]
V
_ * _ [in AAC_tactics.Caveats]_ == _ [in AAC_tactics.Caveats]
1 [in AAC_tactics.Caveats]
other
_ ++ _ [in AAC_tactics.Utils]_ :: _ [in AAC_tactics.Utils]
Binder Index
A
A:1 [in AAC_tactics.AAC]A:11 [in AAC_tactics.Utils]
A:156 [in AAC_tactics.AAC]
A:159 [in AAC_tactics.AAC]
a:16 [in AAC_tactics.Caveats]
A:163 [in AAC_tactics.AAC]
A:20 [in AAC_tactics.Utils]
a:248 [in AAC_tactics.AAC]
a:25 [in AAC_tactics.Caveats]
a:28 [in AAC_tactics.Caveats]
a:308 [in AAC_tactics.AAC]
a:322 [in AAC_tactics.AAC]
a:33 [in AAC_tactics.Caveats]
a:35 [in AAC_tactics.Caveats]
A:36 [in AAC_tactics.Utils]
A:39 [in AAC_tactics.Utils]
a:39 [in AAC_tactics.Caveats]
A:4 [in AAC_tactics.Instances]
A:42 [in AAC_tactics.Utils]
a:46 [in AAC_tactics.Caveats]
A:47 [in AAC_tactics.Utils]
a:47 [in AAC_tactics.Caveats]
A:5 [in AAC_tactics.Instances]
A:50 [in AAC_tactics.Utils]
A:53 [in AAC_tactics.Utils]
A:56 [in AAC_tactics.Utils]
A:6 [in AAC_tactics.Instances]
A:62 [in AAC_tactics.Utils]
A:67 [in AAC_tactics.Utils]
A:7 [in AAC_tactics.Instances]
A:76 [in AAC_tactics.Utils]
A:8 [in AAC_tactics.Instances]
a:84 [in AAC_tactics.Tutorial]
A:9 [in AAC_tactics.Instances]
B
B:12 [in AAC_tactics.Utils]B:160 [in AAC_tactics.AAC]
B:164 [in AAC_tactics.AAC]
b:17 [in AAC_tactics.Caveats]
b:26 [in AAC_tactics.Caveats]
b:29 [in AAC_tactics.Caveats]
b:34 [in AAC_tactics.Caveats]
b:36 [in AAC_tactics.Caveats]
B:40 [in AAC_tactics.Utils]
b:40 [in AAC_tactics.Caveats]
B:44 [in AAC_tactics.Utils]
B:57 [in AAC_tactics.Utils]
B:77 [in AAC_tactics.Utils]
b:85 [in AAC_tactics.Tutorial]
C
Comm:282 [in AAC_tactics.AAC]compare:78 [in AAC_tactics.Utils]
c:27 [in AAC_tactics.Caveats]
c:41 [in AAC_tactics.Caveats]
D
dot_Proper:75 [in AAC_tactics.Caveats]dot_A:74 [in AAC_tactics.Caveats]
dot_Proper:61 [in AAC_tactics.Caveats]
dot_A:60 [in AAC_tactics.Caveats]
dot_Proper:16 [in AAC_tactics.Tutorial]
dot_A:13 [in AAC_tactics.Tutorial]
dot:10 [in AAC_tactics.Tutorial]
dot:59 [in AAC_tactics.Caveats]
dot:7 [in AAC_tactics.AAC]
dot:73 [in AAC_tactics.Caveats]
E
E:3 [in AAC_tactics.Caveats]E:37 [in AAC_tactics.AAC]
E:43 [in AAC_tactics.AAC]
E:49 [in AAC_tactics.AAC]
E:58 [in AAC_tactics.Caveats]
E:72 [in AAC_tactics.Caveats]
E:8 [in AAC_tactics.Tutorial]
E:99 [in AAC_tactics.AAC]
F
f:138 [in AAC_tactics.AAC]f:139 [in AAC_tactics.AAC]
f:334 [in AAC_tactics.AAC]
f:58 [in AAC_tactics.Utils]
G
g:19 [in AAC_tactics.Caveats]H
HER:46 [in AAC_tactics.AAC]HE:44 [in AAC_tactics.AAC]
HE:50 [in AAC_tactics.AAC]
Hnorm:284 [in AAC_tactics.AAC]
Hnorm:327 [in AAC_tactics.AAC]
HP:31 [in AAC_tactics.Caveats]
HR:359 [in AAC_tactics.AAC]
HR:45 [in AAC_tactics.AAC]
HR:51 [in AAC_tactics.AAC]
HR:54 [in AAC_tactics.AAC]
h1:100 [in AAC_tactics.Utils]
H:146 [in AAC_tactics.AAC]
H:228 [in AAC_tactics.AAC]
H:230 [in AAC_tactics.AAC]
h:258 [in AAC_tactics.AAC]
h:259 [in AAC_tactics.AAC]
H:274 [in AAC_tactics.AAC]
h:285 [in AAC_tactics.AAC]
h:286 [in AAC_tactics.AAC]
h:287 [in AAC_tactics.AAC]
H:3 [in AAC_tactics.Instances]
h:310 [in AAC_tactics.AAC]
h:318 [in AAC_tactics.AAC]
h:328 [in AAC_tactics.AAC]
h:329 [in AAC_tactics.AAC]
h:330 [in AAC_tactics.AAC]
H:344 [in AAC_tactics.AAC]
H:352 [in AAC_tactics.AAC]
H:37 [in AAC_tactics.Utils]
H:46 [in AAC_tactics.Utils]
h:71 [in AAC_tactics.Utils]
H:87 [in AAC_tactics.AAC]
h:88 [in AAC_tactics.Utils]
h:95 [in AAC_tactics.Utils]
I
Idem:289 [in AAC_tactics.AAC]Idem:293 [in AAC_tactics.AAC]
insert_aux:104 [in AAC_tactics.Utils]
is_unit:217 [in AAC_tactics.AAC]
is_unit:211 [in AAC_tactics.AAC]
i:1 [in AAC_tactics.Utils]
i:114 [in AAC_tactics.AAC]
i:118 [in AAC_tactics.AAC]
i:129 [in AAC_tactics.AAC]
i:141 [in AAC_tactics.AAC]
i:149 [in AAC_tactics.AAC]
i:152 [in AAC_tactics.AAC]
i:154 [in AAC_tactics.AAC]
i:155 [in AAC_tactics.AAC]
i:18 [in AAC_tactics.Utils]
i:209 [in AAC_tactics.AAC]
i:215 [in AAC_tactics.AAC]
i:219 [in AAC_tactics.AAC]
i:225 [in AAC_tactics.AAC]
i:227 [in AAC_tactics.AAC]
i:229 [in AAC_tactics.AAC]
i:23 [in AAC_tactics.Utils]
i:231 [in AAC_tactics.AAC]
i:232 [in AAC_tactics.AAC]
i:24 [in AAC_tactics.Utils]
i:26 [in AAC_tactics.Utils]
i:28 [in AAC_tactics.Utils]
i:280 [in AAC_tactics.AAC]
i:288 [in AAC_tactics.AAC]
i:292 [in AAC_tactics.AAC]
i:30 [in AAC_tactics.Utils]
i:325 [in AAC_tactics.AAC]
i:332 [in AAC_tactics.AAC]
i:6 [in AAC_tactics.Utils]
J
j:119 [in AAC_tactics.AAC]j:144 [in AAC_tactics.AAC]
j:151 [in AAC_tactics.AAC]
j:19 [in AAC_tactics.Utils]
j:2 [in AAC_tactics.Utils]
j:226 [in AAC_tactics.AAC]
j:235 [in AAC_tactics.AAC]
j:239 [in AAC_tactics.AAC]
j:241 [in AAC_tactics.AAC]
j:25 [in AAC_tactics.Utils]
j:27 [in AAC_tactics.Utils]
j:270 [in AAC_tactics.AAC]
j:29 [in AAC_tactics.Utils]
j:297 [in AAC_tactics.AAC]
j:301 [in AAC_tactics.AAC]
j:303 [in AAC_tactics.AAC]
j:31 [in AAC_tactics.Utils]
j:7 [in AAC_tactics.Utils]
K
k:18 [in AAC_tactics.Caveats]k:260 [in AAC_tactics.AAC]
k:311 [in AAC_tactics.AAC]
k:72 [in AAC_tactics.Utils]
k:89 [in AAC_tactics.Utils]
k:96 [in AAC_tactics.Utils]
L
l':167 [in AAC_tactics.AAC]l':64 [in AAC_tactics.Utils]
l1:105 [in AAC_tactics.Utils]
l2:101 [in AAC_tactics.Utils]
l2:108 [in AAC_tactics.Utils]
l2:109 [in AAC_tactics.Utils]
l:11 [in AAC_tactics.Instances]
l:117 [in AAC_tactics.Utils]
l:121 [in AAC_tactics.Utils]
l:126 [in AAC_tactics.Utils]
l:150 [in AAC_tactics.AAC]
l:166 [in AAC_tactics.AAC]
l:176 [in AAC_tactics.AAC]
l:184 [in AAC_tactics.AAC]
l:186 [in AAC_tactics.AAC]
l:188 [in AAC_tactics.AAC]
l:200 [in AAC_tactics.AAC]
l:202 [in AAC_tactics.AAC]
l:204 [in AAC_tactics.AAC]
l:210 [in AAC_tactics.AAC]
l:216 [in AAC_tactics.AAC]
l:220 [in AAC_tactics.AAC]
l:240 [in AAC_tactics.AAC]
l:245 [in AAC_tactics.AAC]
l:249 [in AAC_tactics.AAC]
l:262 [in AAC_tactics.AAC]
l:266 [in AAC_tactics.AAC]
l:272 [in AAC_tactics.AAC]
l:302 [in AAC_tactics.AAC]
l:306 [in AAC_tactics.AAC]
l:309 [in AAC_tactics.AAC]
l:320 [in AAC_tactics.AAC]
l:333 [in AAC_tactics.AAC]
l:59 [in AAC_tactics.Utils]
l:63 [in AAC_tactics.Utils]
M
map:3 [in AAC_tactics.AAC]merge_aux:112 [in AAC_tactics.Utils]
merge:165 [in AAC_tactics.AAC]
m:253 [in AAC_tactics.AAC]
m:268 [in AAC_tactics.AAC]
m:294 [in AAC_tactics.AAC]
m:315 [in AAC_tactics.AAC]
m:69 [in AAC_tactics.AAC]
N
norm:185 [in AAC_tactics.AAC]norm:201 [in AAC_tactics.AAC]
norm:208 [in AAC_tactics.AAC]
norm:214 [in AAC_tactics.AAC]
norm:281 [in AAC_tactics.AAC]
null:2 [in AAC_tactics.AAC]
n1:99 [in AAC_tactics.Utils]
n:11 [in AAC_tactics.Caveats]
n:115 [in AAC_tactics.AAC]
n:14 [in AAC_tactics.Caveats]
n:175 [in AAC_tactics.AAC]
n:181 [in AAC_tactics.AAC]
n:183 [in AAC_tactics.AAC]
n:247 [in AAC_tactics.AAC]
n:255 [in AAC_tactics.AAC]
n:257 [in AAC_tactics.AAC]
n:261 [in AAC_tactics.AAC]
n:265 [in AAC_tactics.AAC]
n:267 [in AAC_tactics.AAC]
n:271 [in AAC_tactics.AAC]
n:275 [in AAC_tactics.AAC]
n:278 [in AAC_tactics.AAC]
n:290 [in AAC_tactics.AAC]
n:4 [in AAC_tactics.AAC]
n:59 [in AAC_tactics.AAC]
n:65 [in AAC_tactics.AAC]
n:68 [in AAC_tactics.AAC]
n:72 [in AAC_tactics.AAC]
n:74 [in AAC_tactics.AAC]
n:77 [in AAC_tactics.AAC]
n:80 [in AAC_tactics.AAC]
O
one:12 [in AAC_tactics.Tutorial]One:19 [in AAC_tactics.Tutorial]
one:62 [in AAC_tactics.Caveats]
One:63 [in AAC_tactics.Caveats]
one:76 [in AAC_tactics.Caveats]
One:77 [in AAC_tactics.Caveats]
op':57 [in AAC_tactics.AAC]
op:28 [in AAC_tactics.AAC]
op:56 [in AAC_tactics.AAC]
o:134 [in AAC_tactics.AAC]
P
plus_Proper:7 [in AAC_tactics.Caveats]plus_C:6 [in AAC_tactics.Caveats]
plus_A:5 [in AAC_tactics.Caveats]
plus_Proper:17 [in AAC_tactics.Tutorial]
plus_C:15 [in AAC_tactics.Tutorial]
plus_A:14 [in AAC_tactics.Tutorial]
plus:15 [in AAC_tactics.AAC]
plus:22 [in AAC_tactics.AAC]
plus:4 [in AAC_tactics.Caveats]
plus:55 [in AAC_tactics.AAC]
plus:9 [in AAC_tactics.Tutorial]
po:58 [in AAC_tactics.AAC]
p:153 [in AAC_tactics.AAC]
p:269 [in AAC_tactics.AAC]
P:30 [in AAC_tactics.Caveats]
p:319 [in AAC_tactics.AAC]
R
R:13 [in AAC_tactics.Utils]R:14 [in AAC_tactics.AAC]
R:2 [in AAC_tactics.Caveats]
R:2 [in AAC_tactics.Instances]
R:21 [in AAC_tactics.AAC]
R:27 [in AAC_tactics.AAC]
r:273 [in AAC_tactics.AAC]
r:321 [in AAC_tactics.AAC]
R:36 [in AAC_tactics.AAC]
R:42 [in AAC_tactics.AAC]
R:48 [in AAC_tactics.AAC]
R:53 [in AAC_tactics.AAC]
R:57 [in AAC_tactics.Caveats]
R:6 [in AAC_tactics.AAC]
R:7 [in AAC_tactics.Tutorial]
R:71 [in AAC_tactics.Caveats]
R:76 [in AAC_tactics.AAC]
R:90 [in AAC_tactics.AAC]
R:98 [in AAC_tactics.AAC]
S
S:343 [in AAC_tactics.AAC]T
T:24 [in AAC_tactics.Instances]T:25 [in AAC_tactics.Instances]
T:26 [in AAC_tactics.Instances]
T:27 [in AAC_tactics.Instances]
T:28 [in AAC_tactics.Instances]
T:29 [in AAC_tactics.Instances]
T:30 [in AAC_tactics.Instances]
T:31 [in AAC_tactics.Instances]
T:32 [in AAC_tactics.Instances]
T:33 [in AAC_tactics.Instances]
T:34 [in AAC_tactics.Instances]
T:35 [in AAC_tactics.Instances]
T:36 [in AAC_tactics.Instances]
T:37 [in AAC_tactics.Instances]
T:38 [in AAC_tactics.Instances]
T:39 [in AAC_tactics.Instances]
T:40 [in AAC_tactics.Instances]
T:41 [in AAC_tactics.Instances]
T:42 [in AAC_tactics.Instances]
U
unit:29 [in AAC_tactics.AAC]un:135 [in AAC_tactics.AAC]
un:187 [in AAC_tactics.AAC]
un:190 [in AAC_tactics.AAC]
un:79 [in AAC_tactics.Utils]
us:120 [in AAC_tactics.AAC]
us:142 [in AAC_tactics.AAC]
u:102 [in AAC_tactics.AAC]
u:116 [in AAC_tactics.AAC]
u:128 [in AAC_tactics.AAC]
u:140 [in AAC_tactics.AAC]
u:171 [in AAC_tactics.AAC]
u:173 [in AAC_tactics.AAC]
u:180 [in AAC_tactics.AAC]
u:182 [in AAC_tactics.AAC]
u:194 [in AAC_tactics.AAC]
u:196 [in AAC_tactics.AAC]
u:198 [in AAC_tactics.AAC]
u:199 [in AAC_tactics.AAC]
u:203 [in AAC_tactics.AAC]
u:205 [in AAC_tactics.AAC]
u:218 [in AAC_tactics.AAC]
u:242 [in AAC_tactics.AAC]
u:243 [in AAC_tactics.AAC]
u:277 [in AAC_tactics.AAC]
u:283 [in AAC_tactics.AAC]
u:304 [in AAC_tactics.AAC]
u:305 [in AAC_tactics.AAC]
u:323 [in AAC_tactics.AAC]
u:326 [in AAC_tactics.AAC]
u:331 [in AAC_tactics.AAC]
u:337 [in AAC_tactics.AAC]
u:339 [in AAC_tactics.AAC]
u:34 [in AAC_tactics.Utils]
u:341 [in AAC_tactics.AAC]
u:345 [in AAC_tactics.AAC]
u:38 [in AAC_tactics.Utils]
u:43 [in AAC_tactics.Utils]
u:48 [in AAC_tactics.Utils]
u:51 [in AAC_tactics.Utils]
u:85 [in AAC_tactics.Utils]
u:92 [in AAC_tactics.Utils]
V
vm:178 [in AAC_tactics.AAC]vm:263 [in AAC_tactics.AAC]
vm:80 [in AAC_tactics.Utils]
vs:121 [in AAC_tactics.AAC]
vs:145 [in AAC_tactics.AAC]
v:117 [in AAC_tactics.AAC]
v:130 [in AAC_tactics.AAC]
v:143 [in AAC_tactics.AAC]
v:338 [in AAC_tactics.AAC]
v:340 [in AAC_tactics.AAC]
v:342 [in AAC_tactics.AAC]
v:346 [in AAC_tactics.AAC]
v:35 [in AAC_tactics.Utils]
v:45 [in AAC_tactics.Utils]
v:49 [in AAC_tactics.Utils]
v:52 [in AAC_tactics.Utils]
v:86 [in AAC_tactics.Utils]
v:93 [in AAC_tactics.Utils]
X
xn:63 [in AAC_tactics.AAC]xn:64 [in AAC_tactics.AAC]
xn:67 [in AAC_tactics.AAC]
X:1 [in AAC_tactics.Caveats]
X:1 [in AAC_tactics.Instances]
x:10 [in AAC_tactics.Instances]
x:113 [in AAC_tactics.Utils]
x:12 [in AAC_tactics.Caveats]
x:12 [in AAC_tactics.Instances]
X:13 [in AAC_tactics.AAC]
x:13 [in AAC_tactics.Instances]
x:14 [in AAC_tactics.Utils]
x:17 [in AAC_tactics.AAC]
x:17 [in AAC_tactics.Instances]
x:19 [in AAC_tactics.Instances]
X:20 [in AAC_tactics.AAC]
x:20 [in AAC_tactics.Caveats]
x:20 [in AAC_tactics.Tutorial]
x:206 [in AAC_tactics.AAC]
x:212 [in AAC_tactics.AAC]
x:22 [in AAC_tactics.Instances]
x:24 [in AAC_tactics.AAC]
x:246 [in AAC_tactics.AAC]
x:252 [in AAC_tactics.AAC]
x:254 [in AAC_tactics.AAC]
x:256 [in AAC_tactics.AAC]
X:26 [in AAC_tactics.AAC]
x:276 [in AAC_tactics.AAC]
x:279 [in AAC_tactics.AAC]
x:291 [in AAC_tactics.AAC]
x:307 [in AAC_tactics.AAC]
x:31 [in AAC_tactics.AAC]
x:31 [in AAC_tactics.Tutorial]
x:314 [in AAC_tactics.AAC]
x:316 [in AAC_tactics.AAC]
x:317 [in AAC_tactics.AAC]
x:324 [in AAC_tactics.AAC]
x:33 [in AAC_tactics.AAC]
x:347 [in AAC_tactics.AAC]
X:35 [in AAC_tactics.AAC]
x:354 [in AAC_tactics.AAC]
x:357 [in AAC_tactics.AAC]
x:360 [in AAC_tactics.AAC]
x:37 [in AAC_tactics.Caveats]
x:37 [in AAC_tactics.Tutorial]
x:4 [in AAC_tactics.Tutorial]
X:41 [in AAC_tactics.AAC]
x:42 [in AAC_tactics.Caveats]
x:43 [in AAC_tactics.Tutorial]
x:44 [in AAC_tactics.Caveats]
x:46 [in AAC_tactics.Tutorial]
X:47 [in AAC_tactics.AAC]
x:49 [in AAC_tactics.Caveats]
X:5 [in AAC_tactics.AAC]
X:52 [in AAC_tactics.AAC]
x:52 [in AAC_tactics.Caveats]
x:52 [in AAC_tactics.Tutorial]
x:54 [in AAC_tactics.Caveats]
x:55 [in AAC_tactics.Tutorial]
X:56 [in AAC_tactics.Caveats]
X:6 [in AAC_tactics.Tutorial]
x:60 [in AAC_tactics.AAC]
x:60 [in AAC_tactics.Tutorial]
x:62 [in AAC_tactics.Tutorial]
x:66 [in AAC_tactics.AAC]
x:66 [in AAC_tactics.Caveats]
x:68 [in AAC_tactics.Caveats]
x:69 [in AAC_tactics.Tutorial]
x:70 [in AAC_tactics.AAC]
X:70 [in AAC_tactics.Caveats]
x:71 [in AAC_tactics.AAC]
x:73 [in AAC_tactics.AAC]
x:73 [in AAC_tactics.Tutorial]
x:74 [in AAC_tactics.Tutorial]
X:75 [in AAC_tactics.AAC]
x:75 [in AAC_tactics.Tutorial]
x:76 [in AAC_tactics.Tutorial]
x:78 [in AAC_tactics.Caveats]
x:81 [in AAC_tactics.Tutorial]
x:83 [in AAC_tactics.Tutorial]
x:86 [in AAC_tactics.Tutorial]
x:88 [in AAC_tactics.AAC]
x:88 [in AAC_tactics.Tutorial]
X:89 [in AAC_tactics.AAC]
x:89 [in AAC_tactics.Caveats]
x:9 [in AAC_tactics.AAC]
x:90 [in AAC_tactics.Tutorial]
x:91 [in AAC_tactics.Caveats]
x:93 [in AAC_tactics.Caveats]
X:97 [in AAC_tactics.AAC]
Y
y':80 [in AAC_tactics.Caveats]y:10 [in AAC_tactics.AAC]
y:15 [in AAC_tactics.Utils]
y:18 [in AAC_tactics.AAC]
y:18 [in AAC_tactics.Instances]
y:20 [in AAC_tactics.Instances]
y:21 [in AAC_tactics.Caveats]
y:23 [in AAC_tactics.Instances]
y:32 [in AAC_tactics.Tutorial]
y:348 [in AAC_tactics.AAC]
y:353 [in AAC_tactics.AAC]
y:356 [in AAC_tactics.AAC]
y:361 [in AAC_tactics.AAC]
y:44 [in AAC_tactics.Tutorial]
y:50 [in AAC_tactics.Caveats]
y:53 [in AAC_tactics.Tutorial]
y:63 [in AAC_tactics.Tutorial]
y:70 [in AAC_tactics.Tutorial]
y:79 [in AAC_tactics.Caveats]
y:82 [in AAC_tactics.Tutorial]
y:87 [in AAC_tactics.Tutorial]
y:89 [in AAC_tactics.Tutorial]
y:94 [in AAC_tactics.Caveats]
Z
zero:11 [in AAC_tactics.Tutorial]Zero:18 [in AAC_tactics.Tutorial]
zero:8 [in AAC_tactics.Caveats]
Zero:9 [in AAC_tactics.Caveats]
z:11 [in AAC_tactics.AAC]
z:21 [in AAC_tactics.Instances]
z:355 [in AAC_tactics.AAC]
z:358 [in AAC_tactics.AAC]
z:64 [in AAC_tactics.Tutorial]
z:71 [in AAC_tactics.Tutorial]
Module Index
A
All [in AAC_tactics.Instances]B
Bool [in AAC_tactics.Instances]I
Internal [in AAC_tactics.AAC]Internal.Bin [in AAC_tactics.AAC]
Internal.Sym [in AAC_tactics.AAC]
L
Lists [in AAC_tactics.Instances]N
N [in AAC_tactics.Instances]P
P [in AAC_tactics.Instances]Peano [in AAC_tactics.Instances]
Prop_ops [in AAC_tactics.Instances]
Q
Q [in AAC_tactics.Instances]R
Relations [in AAC_tactics.Instances]Z
Z [in AAC_tactics.Instances]Variable Index
A
AAC_normalise.d [in AAC_tactics.Tutorial]AAC_normalise.c [in AAC_tactics.Tutorial]
AAC_normalise.b [in AAC_tactics.Tutorial]
AAC_normalise.a [in AAC_tactics.Tutorial]
B
base.both.a [in AAC_tactics.Tutorial]base.both.b [in AAC_tactics.Tutorial]
base.both.c [in AAC_tactics.Tutorial]
base.both.d [in AAC_tactics.Tutorial]
base.both.H [in AAC_tactics.Tutorial]
base.both.H' [in AAC_tactics.Tutorial]
base.dealing_with_units.H' [in AAC_tactics.Tutorial]
base.dealing_with_units.H [in AAC_tactics.Tutorial]
base.dealing_with_units.c [in AAC_tactics.Tutorial]
base.dealing_with_units.b [in AAC_tactics.Tutorial]
base.dealing_with_units.a [in AAC_tactics.Tutorial]
base.morphisms.a [in AAC_tactics.Tutorial]
base.morphisms.b [in AAC_tactics.Tutorial]
base.morphisms.f [in AAC_tactics.Tutorial]
base.morphisms.g [in AAC_tactics.Tutorial]
base.morphisms.H [in AAC_tactics.Tutorial]
base.morphisms.Hf [in AAC_tactics.Tutorial]
base.morphisms.Hg [in AAC_tactics.Tutorial]
base.occurrence.a [in AAC_tactics.Tutorial]
base.occurrence.f [in AAC_tactics.Tutorial]
base.occurrence.H [in AAC_tactics.Tutorial]
base.occurrence.Hf [in AAC_tactics.Tutorial]
base.reminder.a [in AAC_tactics.Tutorial]
base.reminder.b [in AAC_tactics.Tutorial]
base.reminder.c [in AAC_tactics.Tutorial]
base.reminder.H [in AAC_tactics.Tutorial]
base.subst.a [in AAC_tactics.Tutorial]
base.subst.b [in AAC_tactics.Tutorial]
base.subst.c [in AAC_tactics.Tutorial]
base.subst.d [in AAC_tactics.Tutorial]
base.subst.H [in AAC_tactics.Tutorial]
base.subst.H' [in AAC_tactics.Tutorial]
D
dep.f [in AAC_tactics.Utils]dep.T [in AAC_tactics.Utils]
dep.U [in AAC_tactics.Utils]
E
evars.H [in AAC_tactics.Caveats]evars.H' [in AAC_tactics.Caveats]
evars.idem [in AAC_tactics.Caveats]
evars.P [in AAC_tactics.Caveats]
Examples.a [in AAC_tactics.Tutorial]
Examples.b [in AAC_tactics.Tutorial]
Examples.c [in AAC_tactics.Tutorial]
Examples.H [in AAC_tactics.Tutorial]
I
ineq.H [in AAC_tactics.Caveats]Internal.s.e_unit [in AAC_tactics.AAC]
Internal.s.e_bin [in AAC_tactics.AAC]
Internal.s.e_sym [in AAC_tactics.AAC]
Internal.s.prds.i [in AAC_tactics.AAC]
Internal.s.prds.is_unit [in AAC_tactics.AAC]
Internal.s.prd_correctness.is_unit_prd_Unit [in AAC_tactics.AAC]
Internal.s.prd_correctness.is_unit [in AAC_tactics.AAC]
Internal.s.prd_correctness.i [in AAC_tactics.AAC]
Internal.s.sums.i [in AAC_tactics.AAC]
Internal.s.sums.is_unit [in AAC_tactics.AAC]
Internal.s.sum_correctness.comm [in AAC_tactics.AAC]
Internal.s.sum_correctness.is_unit_sum_Unit [in AAC_tactics.AAC]
Internal.s.sum_correctness.is_unit [in AAC_tactics.AAC]
Internal.s.sum_correctness.i [in AAC_tactics.AAC]
introduction.a [in AAC_tactics.Tutorial]
introduction.b [in AAC_tactics.Tutorial]
introduction.c [in AAC_tactics.Tutorial]
introduction.H [in AAC_tactics.Tutorial]
L
lists.c.A [in AAC_tactics.Utils]lists.c.B [in AAC_tactics.Utils]
lists.c.compare [in AAC_tactics.Utils]
Lists.H [in AAC_tactics.Tutorial]
lists.list_compare_weak_spec.Hcompare [in AAC_tactics.Utils]
lists.list_compare_weak_spec.compare [in AAC_tactics.Utils]
lists.list_compare_weak_spec.A [in AAC_tactics.Utils]
Lists.l1 [in AAC_tactics.Tutorial]
Lists.l2 [in AAC_tactics.Tutorial]
Lists.l3 [in AAC_tactics.Tutorial]
lists.mset_compare_weak_spec.Hcompare [in AAC_tactics.Utils]
lists.mset_compare_weak_spec.compare [in AAC_tactics.Utils]
lists.mset_compare_weak_spec.A [in AAC_tactics.Utils]
lists.m.A [in AAC_tactics.Utils]
lists.m.B [in AAC_tactics.Utils]
lists.m.bind [in AAC_tactics.Utils]
lists.m.b2 [in AAC_tactics.Utils]
lists.m.compare [in AAC_tactics.Utils]
lists.m.map [in AAC_tactics.Utils]
lists.m.merge [in AAC_tactics.Utils]
lists.m.ret [in AAC_tactics.Utils]
Lists.X [in AAC_tactics.Tutorial]
M
morphism.H [in AAC_tactics.Caveats]P
parameters.f [in AAC_tactics.Caveats]parameters.g [in AAC_tactics.Caveats]
parameters.H [in AAC_tactics.Caveats]
parameters.Hf [in AAC_tactics.Caveats]
parameters.Hf' [in AAC_tactics.Caveats]
parameters.Hg [in AAC_tactics.Caveats]
Peano.a [in AAC_tactics.Tutorial]
Peano.b [in AAC_tactics.Tutorial]
Peano.c [in AAC_tactics.Tutorial]
Peano.H [in AAC_tactics.Caveats]
Peano.H [in AAC_tactics.Tutorial]
Peano.H' [in AAC_tactics.Caveats]
R
Relations.defs.R [in AAC_tactics.Instances]Relations.defs.S [in AAC_tactics.Instances]
Relations.defs.T [in AAC_tactics.Instances]
U
U.dot_inv_right [in AAC_tactics.Caveats]U.dot_inv_left [in AAC_tactics.Caveats]
U.f [in AAC_tactics.Caveats]
U.Hf [in AAC_tactics.Caveats]
W
W.a [in AAC_tactics.Caveats]W.b [in AAC_tactics.Caveats]
W.c [in AAC_tactics.Caveats]
W.H [in AAC_tactics.Caveats]
Z
Z.a [in AAC_tactics.Caveats]Z.b [in AAC_tactics.Caveats]
Z.c [in AAC_tactics.Caveats]
Z.f [in AAC_tactics.Caveats]
Z.H [in AAC_tactics.Caveats]
Z.H0 [in AAC_tactics.Caveats]
Z.H1 [in AAC_tactics.Caveats]
Library Index
A
AACC
CaveatsConstants
I
InstancesT
TutorialU
UtilsLemma Index
C
cast_eq [in AAC_tactics.Utils]E
eq_idx_spec [in AAC_tactics.Utils]eq_subr [in AAC_tactics.Instances]
H
Hbin1 [in AAC_tactics.Tutorial]Hbin2 [in AAC_tactics.Tutorial]
Hopp [in AAC_tactics.Tutorial]
I
idx_compare_reflect_eq [in AAC_tactics.Utils]Internal.compare_reflect_eq [in AAC_tactics.AAC]
Internal.compat_prd_unit_add [in AAC_tactics.AAC]
Internal.compat_prd_unit_return [in AAC_tactics.AAC]
Internal.compat_sum_unit_add [in AAC_tactics.AAC]
Internal.compat_sum_unit_return [in AAC_tactics.AAC]
Internal.copy_idem [in AAC_tactics.AAC]
Internal.copy_n_unit [in AAC_tactics.AAC]
Internal.copy_mset_copy [in AAC_tactics.AAC]
Internal.copy_mset_succ [in AAC_tactics.AAC]
Internal.copy_mset' [in AAC_tactics.AAC]
Internal.copy_Psucc [in AAC_tactics.AAC]
Internal.copy_xH [in AAC_tactics.AAC]
Internal.copy_plus [in AAC_tactics.AAC]
Internal.decide [in AAC_tactics.AAC]
Internal.eval_norm_lists [in AAC_tactics.AAC]
Internal.eval_prd_app [in AAC_tactics.AAC]
Internal.eval_prd_cons [in AAC_tactics.AAC]
Internal.eval_prd_nil [in AAC_tactics.AAC]
Internal.eval_reduce_msets [in AAC_tactics.AAC]
Internal.eval_norm_msets [in AAC_tactics.AAC]
Internal.eval_merge_bin [in AAC_tactics.AAC]
Internal.eval_sum_cons [in AAC_tactics.AAC]
Internal.eval_sum_nil [in AAC_tactics.AAC]
Internal.is_prd_spec [in AAC_tactics.AAC]
Internal.is_sum_spec [in AAC_tactics.AAC]
Internal.is_unit_of_Unit [in AAC_tactics.AAC]
Internal.lift_normalise [in AAC_tactics.AAC]
Internal.normalise [in AAC_tactics.AAC]
Internal.prd'_prd [in AAC_tactics.AAC]
Internal.sum'_sum [in AAC_tactics.AAC]
Internal.z0 [in AAC_tactics.AAC]
Internal.z0' [in AAC_tactics.AAC]
Internal.z1 [in AAC_tactics.AAC]
Internal.z1' [in AAC_tactics.AAC]
Internal.z2 [in AAC_tactics.AAC]
Internal.z2' [in AAC_tactics.AAC]
inv_unique [in AAC_tactics.Caveats]
L
lift_reflexivity [in AAC_tactics.AAC]lift_transitivity_right [in AAC_tactics.AAC]
lift_transitivity_left [in AAC_tactics.AAC]
list_compare_weak_spec [in AAC_tactics.Utils]
M
mset_compare_weak_spec [in AAC_tactics.Utils]P
pos_compare_weak_spec [in AAC_tactics.Utils]P.Pmult_1_l [in AAC_tactics.Instances]
R
reflect_eqdep_weak_spec [in AAC_tactics.Utils]reflect_eqdep_eq [in AAC_tactics.Utils]
Z
Zabs_triangle [in AAC_tactics.Tutorial]Zplus_opp_r [in AAC_tactics.Tutorial]
Constructor Index
C
cons [in AAC_tactics.Utils]D
decide_false [in AAC_tactics.Utils]decide_true [in AAC_tactics.Utils]
I
Internal.Bin.mk_pack [in AAC_tactics.AAC]Internal.cpu_right [in AAC_tactics.AAC]
Internal.cpu_left [in AAC_tactics.AAC]
Internal.csu_right [in AAC_tactics.AAC]
Internal.csu_left [in AAC_tactics.AAC]
Internal.is_prd_spec_nothing [in AAC_tactics.AAC]
Internal.is_prd_spec_unit [in AAC_tactics.AAC]
Internal.is_prd_spec_op [in AAC_tactics.AAC]
Internal.is_sum_spec_nothing [in AAC_tactics.AAC]
Internal.is_sum_spec_unit [in AAC_tactics.AAC]
Internal.is_sum_spec_op [in AAC_tactics.AAC]
Internal.Is_nothing [in AAC_tactics.AAC]
Internal.Is_unit [in AAC_tactics.AAC]
Internal.Is_op [in AAC_tactics.AAC]
Internal.left [in AAC_tactics.AAC]
Internal.mk_unit_pack [in AAC_tactics.AAC]
Internal.mk_unit_for [in AAC_tactics.AAC]
Internal.prd [in AAC_tactics.AAC]
Internal.right [in AAC_tactics.AAC]
Internal.sum [in AAC_tactics.AAC]
Internal.sym [in AAC_tactics.AAC]
Internal.Sym.mkPack [in AAC_tactics.AAC]
Internal.unit [in AAC_tactics.AAC]
Internal.vcons [in AAC_tactics.AAC]
Internal.vnil [in AAC_tactics.AAC]
L
law_idem [in AAC_tactics.AAC]law_comm [in AAC_tactics.AAC]
law_assoc [in AAC_tactics.AAC]
N
nil [in AAC_tactics.Utils]P
pcws_gt [in AAC_tactics.Utils]pcws_lt [in AAC_tactics.Utils]
pcws_eq [in AAC_tactics.Utils]
Inductive Index
A
Associative [in AAC_tactics.AAC]C
Commutative [in AAC_tactics.AAC]compare_weak_spec [in AAC_tactics.Utils]
D
decide_spec [in AAC_tactics.Utils]I
Idempotent [in AAC_tactics.AAC]Internal.compat_prd_unit [in AAC_tactics.AAC]
Internal.compat_sum_unit [in AAC_tactics.AAC]
Internal.discr [in AAC_tactics.AAC]
Internal.is_prd_spec_ind [in AAC_tactics.AAC]
Internal.is_sum_spec_ind [in AAC_tactics.AAC]
Internal.m [in AAC_tactics.AAC]
Internal.T [in AAC_tactics.AAC]
Internal.vT [in AAC_tactics.AAC]
N
nelist [in AAC_tactics.Utils]Projection Index
A
aac_list_proper [in AAC_tactics.AAC]aac_lift_equivalence [in AAC_tactics.AAC]
I
Internal.Bin.assoc [in AAC_tactics.AAC]Internal.Bin.comm [in AAC_tactics.AAC]
Internal.Bin.compat [in AAC_tactics.AAC]
Internal.Bin.idem [in AAC_tactics.AAC]
Internal.Bin.value [in AAC_tactics.AAC]
Internal.Sym.ar [in AAC_tactics.AAC]
Internal.Sym.morph [in AAC_tactics.AAC]
Internal.Sym.value [in AAC_tactics.AAC]
Internal.uf_desc [in AAC_tactics.AAC]
Internal.uf_idx [in AAC_tactics.AAC]
Internal.u_desc [in AAC_tactics.AAC]
Internal.u_value [in AAC_tactics.AAC]
L
law_neutral_right [in AAC_tactics.AAC]law_neutral_left [in AAC_tactics.AAC]
law_idem [in AAC_tactics.AAC]
law_comm [in AAC_tactics.AAC]
law_assoc [in AAC_tactics.AAC]
Section Index
A
AAC_normalise [in AAC_tactics.Tutorial]B
base [in AAC_tactics.Tutorial]base.both [in AAC_tactics.Tutorial]
base.dealing_with_units [in AAC_tactics.Tutorial]
base.morphisms [in AAC_tactics.Tutorial]
base.occurrence [in AAC_tactics.Tutorial]
base.reminder [in AAC_tactics.Tutorial]
base.subst [in AAC_tactics.Tutorial]
D
dep [in AAC_tactics.Utils]E
evars [in AAC_tactics.Caveats]Examples [in AAC_tactics.Tutorial]
I
ineq [in AAC_tactics.Caveats]Internal.Bin.t [in AAC_tactics.AAC]
Internal.copy [in AAC_tactics.AAC]
Internal.s [in AAC_tactics.AAC]
Internal.Sym.t [in AAC_tactics.AAC]
Internal.s.prds [in AAC_tactics.AAC]
Internal.s.prd_correctness [in AAC_tactics.AAC]
Internal.s.sums [in AAC_tactics.AAC]
Internal.s.sum_correctness [in AAC_tactics.AAC]
introduction [in AAC_tactics.Tutorial]
L
lists [in AAC_tactics.Utils]Lists [in AAC_tactics.Tutorial]
lists.c [in AAC_tactics.Utils]
lists.list_compare_weak_spec [in AAC_tactics.Utils]
lists.m [in AAC_tactics.Utils]
lists.mset_compare_weak_spec [in AAC_tactics.Utils]
M
morphism [in AAC_tactics.Caveats]P
parameters [in AAC_tactics.Caveats]Peano [in AAC_tactics.Caveats]
Peano [in AAC_tactics.Tutorial]
R
Relations.defs [in AAC_tactics.Instances]S
sigma [in AAC_tactics.AAC]T
t [in AAC_tactics.AAC]U
U [in AAC_tactics.Caveats]V
V [in AAC_tactics.Caveats]W
W [in AAC_tactics.Caveats]Z
Z [in AAC_tactics.Caveats]Instance Index
A
aac_lift_proper [in AAC_tactics.AAC]aac_lift_subrelation [in AAC_tactics.AAC]
aac_zero_max [in AAC_tactics.Tutorial]
aac_max_Idem [in AAC_tactics.Tutorial]
aac_max_Assoc [in AAC_tactics.Tutorial]
aac_max_Comm [in AAC_tactics.Tutorial]
aac_zero_add [in AAC_tactics.Tutorial]
aac_one [in AAC_tactics.Tutorial]
aac_mul_Assoc [in AAC_tactics.Tutorial]
aac_mul_Comm [in AAC_tactics.Tutorial]
aac_add_Comm [in AAC_tactics.Tutorial]
aac_add_Assoc [in AAC_tactics.Tutorial]
B
Bool.aac_false [in AAC_tactics.Instances]Bool.aac_true [in AAC_tactics.Instances]
Bool.aac_andb_Idem [in AAC_tactics.Instances]
Bool.aac_andb_Comm [in AAC_tactics.Instances]
Bool.aac_andb_Assoc [in AAC_tactics.Instances]
Bool.aac_orb_Idem [in AAC_tactics.Instances]
Bool.aac_orb_Comm [in AAC_tactics.Instances]
Bool.aac_orb_Assoc [in AAC_tactics.Instances]
Bool.negb_compat [in AAC_tactics.Instances]
I
Internal.assoc [in AAC_tactics.AAC]Internal.Binvalue_Proper [in AAC_tactics.AAC]
Internal.Binvalue_Associative [in AAC_tactics.AAC]
Internal.Binvalue_Idempotent [in AAC_tactics.AAC]
Internal.Binvalue_Commutative [in AAC_tactics.AAC]
Internal.compat_prd_Unit [in AAC_tactics.AAC]
Internal.compat_sum_unit_Unit [in AAC_tactics.AAC]
Internal.copy_compat [in AAC_tactics.AAC]
Internal.eval_aux_compat [in AAC_tactics.AAC]
Internal.proper [in AAC_tactics.AAC]
L
lift_le_eq [in AAC_tactics.Tutorial]Lists.aac_nil_Permutation_append [in AAC_tactics.Instances]
Lists.aac_append_Permutation_Comm [in AAC_tactics.Instances]
Lists.aac_append_Permutation_Assoc [in AAC_tactics.Instances]
Lists.aac_append_Proper [in AAC_tactics.Instances]
Lists.aac_nil_append [in AAC_tactics.Instances]
Lists.aac_append_Assoc [in AAC_tactics.Instances]
N
N.aac_zero_max [in AAC_tactics.Instances]N.aac_zero [in AAC_tactics.Instances]
N.aac_one [in AAC_tactics.Instances]
N.aac_Nmax_Idem [in AAC_tactics.Instances]
N.aac_Nmax_Assoc [in AAC_tactics.Instances]
N.aac_Nmax_Comm [in AAC_tactics.Instances]
N.aac_Nmin_Idem [in AAC_tactics.Instances]
N.aac_Nmin_Assoc [in AAC_tactics.Instances]
N.aac_Nmin_Comm [in AAC_tactics.Instances]
N.aac_Nmult_Assoc [in AAC_tactics.Instances]
N.aac_Nmult_Comm [in AAC_tactics.Instances]
N.aac_Nplus_Comm [in AAC_tactics.Instances]
N.aac_Nplus_Assoc [in AAC_tactics.Instances]
N.lift_le_eq [in AAC_tactics.Instances]
N.preorder_le [in AAC_tactics.Instances]
P
Peano.aac_zero_max [in AAC_tactics.Instances]Peano.aac_zero_add [in AAC_tactics.Instances]
Peano.aac_one [in AAC_tactics.Instances]
Peano.aac_max_Idem [in AAC_tactics.Instances]
Peano.aac_max_Assoc [in AAC_tactics.Instances]
Peano.aac_max_Comm [in AAC_tactics.Instances]
Peano.aac_min_Idem [in AAC_tactics.Instances]
Peano.aac_min_Assoc [in AAC_tactics.Instances]
Peano.aac_min_Comm [in AAC_tactics.Instances]
Peano.aac_mul_Assoc [in AAC_tactics.Instances]
Peano.aac_mul_Comm [in AAC_tactics.Instances]
Peano.aac_add_Comm [in AAC_tactics.Instances]
Peano.aac_add_Assoc [in AAC_tactics.Instances]
Peano.lift_le_eq [in AAC_tactics.Instances]
Peano.preorder_le [in AAC_tactics.Instances]
Proper_Zplus [in AAC_tactics.Tutorial]
Prop_ops.lift_impl_iff [in AAC_tactics.Instances]
Prop_ops.aac_not_compat [in AAC_tactics.Instances]
Prop_ops.aac_False [in AAC_tactics.Instances]
Prop_ops.aac_True [in AAC_tactics.Instances]
Prop_ops.aac_and_Idem [in AAC_tactics.Instances]
Prop_ops.aac_or_Idem [in AAC_tactics.Instances]
Prop_ops.aac_or_Comm [in AAC_tactics.Instances]
Prop_ops.aac_or_Assoc [in AAC_tactics.Instances]
P.aac_one_max [in AAC_tactics.Instances]
P.aac_one [in AAC_tactics.Instances]
P.aac_Pmax_Idem [in AAC_tactics.Instances]
P.aac_Pmax_Assoc [in AAC_tactics.Instances]
P.aac_Pmax_Comm [in AAC_tactics.Instances]
P.aac_Pmin_Idem [in AAC_tactics.Instances]
P.aac_Pmin_Assoc [in AAC_tactics.Instances]
P.aac_Pmin_Comm [in AAC_tactics.Instances]
P.aac_Pmult_Assoc [in AAC_tactics.Instances]
P.aac_Pmult_Comm [in AAC_tactics.Instances]
P.aac_Pplus_Comm [in AAC_tactics.Instances]
P.aac_Pplus_Assoc [in AAC_tactics.Instances]
P.lift_le_eq [in AAC_tactics.Instances]
P.preorder_le [in AAC_tactics.Instances]
Q
Q.aac_zero_Qplus [in AAC_tactics.Instances]Q.aac_one [in AAC_tactics.Instances]
Q.aac_Qmax_Idem [in AAC_tactics.Instances]
Q.aac_Qmax_Assoc [in AAC_tactics.Instances]
Q.aac_Qmax_Comm [in AAC_tactics.Instances]
Q.aac_Qmin_Idem [in AAC_tactics.Instances]
Q.aac_Qmin_Assoc [in AAC_tactics.Instances]
Q.aac_Qmin_Comm [in AAC_tactics.Instances]
Q.aac_Qmult_Assoc [in AAC_tactics.Instances]
Q.aac_Qmult_Comm [in AAC_tactics.Instances]
Q.aac_Qplus_Comm [in AAC_tactics.Instances]
Q.aac_Qplus_Assoc [in AAC_tactics.Instances]
Q.lift_le_eq [in AAC_tactics.Instances]
Q.preorder_le [in AAC_tactics.Instances]
R
Relations.aac_eq [in AAC_tactics.Instances]Relations.aac_compo [in AAC_tactics.Instances]
Relations.aac_top [in AAC_tactics.Instances]
Relations.aac_inter_Idem [in AAC_tactics.Instances]
Relations.aac_inter_Assoc [in AAC_tactics.Instances]
Relations.aac_inter_Comm [in AAC_tactics.Instances]
Relations.aac_bot [in AAC_tactics.Instances]
Relations.aac_union_Idem [in AAC_tactics.Instances]
Relations.aac_union_Assoc [in AAC_tactics.Instances]
Relations.aac_union_Comm [in AAC_tactics.Instances]
Relations.clos_refl_trans_compat [in AAC_tactics.Instances]
Relations.clos_refl_trans_incr [in AAC_tactics.Instances]
Relations.clos_trans_compat [in AAC_tactics.Instances]
Relations.clos_trans_incr [in AAC_tactics.Instances]
Relations.eq_same_relation [in AAC_tactics.Instances]
Relations.lift_inclusion_same_relation [in AAC_tactics.Instances]
Relations.negr_compat [in AAC_tactics.Instances]
Relations.preorder_inclusion [in AAC_tactics.Instances]
Relations.transp_compat [in AAC_tactics.Instances]
Z
Zminus_compat [in AAC_tactics.Tutorial]Zplus_incr [in AAC_tactics.Caveats]
Z.aac_zero_Zplus [in AAC_tactics.Instances]
Z.aac_one [in AAC_tactics.Instances]
Z.aac_Zmax_Idem [in AAC_tactics.Instances]
Z.aac_Zmax_Assoc [in AAC_tactics.Instances]
Z.aac_Zmax_Comm [in AAC_tactics.Instances]
Z.aac_Zmin_Idem [in AAC_tactics.Instances]
Z.aac_Zmin_Assoc [in AAC_tactics.Instances]
Z.aac_Zmin_Comm [in AAC_tactics.Instances]
Z.aac_Zmult_Assoc [in AAC_tactics.Instances]
Z.aac_Zmult_Comm [in AAC_tactics.Instances]
Z.aac_Zplus_Comm [in AAC_tactics.Instances]
Z.aac_Zplus_Assoc [in AAC_tactics.Instances]
Z.lift_le_eq [in AAC_tactics.Instances]
Z.preorder_Zle [in AAC_tactics.Instances]
Abbreviation Index
C
cast [in AAC_tactics.Utils]I
idx [in AAC_tactics.Utils]L
lex [in AAC_tactics.Utils]P
pos_compare [in AAC_tactics.Utils]Definition Index
A
appne [in AAC_tactics.Utils]E
eq_idx_bool [in AAC_tactics.Utils]F
fold_map' [in AAC_tactics.Utils]fold_map [in AAC_tactics.Utils]
I
idx_compare [in AAC_tactics.Utils]insert [in AAC_tactics.Utils]
Internal.add_to_prd [in AAC_tactics.AAC]
Internal.add_to_sum [in AAC_tactics.AAC]
Internal.comp [in AAC_tactics.AAC]
Internal.compare [in AAC_tactics.AAC]
Internal.copy [in AAC_tactics.AAC]
Internal.copy_mset [in AAC_tactics.AAC]
Internal.copy' [in AAC_tactics.AAC]
Internal.eval [in AAC_tactics.AAC]
Internal.eval_norm_aux [in AAC_tactics.AAC]
Internal.eval_norm [in AAC_tactics.AAC]
Internal.eval_aux [in AAC_tactics.AAC]
Internal.is_prd [in AAC_tactics.AAC]
Internal.is_sum [in AAC_tactics.AAC]
Internal.is_idempotent [in AAC_tactics.AAC]
Internal.is_commutative [in AAC_tactics.AAC]
Internal.is_unit_of [in AAC_tactics.AAC]
Internal.norm [in AAC_tactics.AAC]
Internal.norm_msets [in AAC_tactics.AAC]
Internal.norm_lists [in AAC_tactics.AAC]
Internal.norm_lists_ [in AAC_tactics.AAC]
Internal.norm_msets_ [in AAC_tactics.AAC]
Internal.prd' [in AAC_tactics.AAC]
Internal.return_prd [in AAC_tactics.AAC]
Internal.return_sum [in AAC_tactics.AAC]
Internal.run_msets [in AAC_tactics.AAC]
Internal.run_list [in AAC_tactics.AAC]
Internal.sum' [in AAC_tactics.AAC]
Internal.Sym.null [in AAC_tactics.AAC]
Internal.Sym.rel_of [in AAC_tactics.AAC]
Internal.Sym.type_of [in AAC_tactics.AAC]
Internal.tcompare_weak_spec [in AAC_tactics.AAC]
Internal.vcompare [in AAC_tactics.AAC]
Internal.vcompare_reflect_eqdep [in AAC_tactics.AAC]
Internal.vnorm [in AAC_tactics.AAC]
L
list_compare [in AAC_tactics.Utils]M
merge_map [in AAC_tactics.Utils]merge_msets [in AAC_tactics.Utils]
mset [in AAC_tactics.Utils]
mset_compare [in AAC_tactics.Utils]
N
nelist_map [in AAC_tactics.Utils]R
reduce_mset [in AAC_tactics.Utils]reflect_eqdep [in AAC_tactics.Utils]
Relations.bot [in AAC_tactics.Instances]
Relations.compo [in AAC_tactics.Instances]
Relations.inter [in AAC_tactics.Instances]
Relations.negr [in AAC_tactics.Instances]
Relations.top [in AAC_tactics.Instances]
S
sigma [in AAC_tactics.AAC]sigma_empty [in AAC_tactics.AAC]
sigma_add [in AAC_tactics.AAC]
sigma_get [in AAC_tactics.AAC]
U
Unnamed_thm5 [in AAC_tactics.Caveats]Unnamed_thm5 [in AAC_tactics.Caveats]
Unnamed_thm5 [in AAC_tactics.Caveats]
Unnamed_thm5 [in AAC_tactics.Caveats]
Unnamed_thm4 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm3 [in AAC_tactics.Caveats]
Unnamed_thm2 [in AAC_tactics.Caveats]
Unnamed_thm1 [in AAC_tactics.Caveats]
Unnamed_thm1 [in AAC_tactics.Caveats]
Unnamed_thm0 [in AAC_tactics.Caveats]
Unnamed_thm [in AAC_tactics.Caveats]
Unnamed_thm24 [in AAC_tactics.Tutorial]
Unnamed_thm23 [in AAC_tactics.Tutorial]
Unnamed_thm22 [in AAC_tactics.Tutorial]
Unnamed_thm21 [in AAC_tactics.Tutorial]
Unnamed_thm20 [in AAC_tactics.Tutorial]
Unnamed_thm20 [in AAC_tactics.Tutorial]
Unnamed_thm20 [in AAC_tactics.Tutorial]
Unnamed_thm19 [in AAC_tactics.Tutorial]
Unnamed_thm18 [in AAC_tactics.Tutorial]
Unnamed_thm17 [in AAC_tactics.Tutorial]
Unnamed_thm16 [in AAC_tactics.Tutorial]
Unnamed_thm15 [in AAC_tactics.Tutorial]
Unnamed_thm14 [in AAC_tactics.Tutorial]
Unnamed_thm13 [in AAC_tactics.Tutorial]
Unnamed_thm12 [in AAC_tactics.Tutorial]
Unnamed_thm11 [in AAC_tactics.Tutorial]
Unnamed_thm11 [in AAC_tactics.Tutorial]
Unnamed_thm10 [in AAC_tactics.Tutorial]
Unnamed_thm9 [in AAC_tactics.Tutorial]
Unnamed_thm8 [in AAC_tactics.Tutorial]
Unnamed_thm7 [in AAC_tactics.Tutorial]
Unnamed_thm6 [in AAC_tactics.Tutorial]
Unnamed_thm5 [in AAC_tactics.Tutorial]
Unnamed_thm4 [in AAC_tactics.Tutorial]
Unnamed_thm3 [in AAC_tactics.Tutorial]
Unnamed_thm2 [in AAC_tactics.Tutorial]
Unnamed_thm1 [in AAC_tactics.Tutorial]
Unnamed_thm0 [in AAC_tactics.Tutorial]
Unnamed_thm [in AAC_tactics.Tutorial]
Record Index
A
AAC_lift [in AAC_tactics.AAC]Associative [in AAC_tactics.AAC]
C
Commutative [in AAC_tactics.AAC]I
Idempotent [in AAC_tactics.AAC]Internal.Bin.pack [in AAC_tactics.AAC]
Internal.Sym.pack [in AAC_tactics.AAC]
Internal.unit_pack [in AAC_tactics.AAC]
Internal.unit_of [in AAC_tactics.AAC]
U
Unit [in AAC_tactics.AAC]Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1064 entries) |
Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (489 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (119 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (55 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (35 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (140 entries) |
Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (104 entries) |
Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
This page has been generated by coqdoc