| 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 | (685 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) |
| 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 | (176 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 | (31 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 | (39 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 | (161 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 | (3 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 | (140 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_le_eq_lift [instance, in AAC_tactics.Tutorial]
aac_Nat_max_0_Unit [instance, in AAC_tactics.Tutorial]
aac_Nat_max_Idem [instance, in AAC_tactics.Tutorial]
aac_Nat_max_Assoc [instance, in AAC_tactics.Tutorial]
aac_Nat_max_Comm [instance, in AAC_tactics.Tutorial]
aac_Nat_add_0_Unit [instance, in AAC_tactics.Tutorial]
aac_Nat_mul_1_Unit [instance, in AAC_tactics.Tutorial]
aac_Nat_mul_Assoc [instance, in AAC_tactics.Tutorial]
aac_Nat_mul_Comm [instance, in AAC_tactics.Tutorial]
aac_Nat_add_Comm [instance, in AAC_tactics.Tutorial]
aac_Nat_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]
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.dot [variable, in AAC_tactics.Tutorial]
base.dot_Proper [variable, in AAC_tactics.Tutorial]
base.dot_A [variable, in AAC_tactics.Tutorial]
base.E [variable, 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.One [variable, in AAC_tactics.Tutorial]
base.one [variable, in AAC_tactics.Tutorial]
base.plus [variable, in AAC_tactics.Tutorial]
base.plus_Proper [variable, in AAC_tactics.Tutorial]
base.plus_C [variable, in AAC_tactics.Tutorial]
base.plus_A [variable, in AAC_tactics.Tutorial]
base.R [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]
base.X [variable, in AAC_tactics.Tutorial]
base.Zero [variable, in AAC_tactics.Tutorial]
base.zero [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_Bool_andb_true_Unit [instance, in AAC_tactics.Instances]
Bool.aac_Bool_orb_false_Unit [instance, in AAC_tactics.Instances]
Bool.aac_Bool_andb_Idem [instance, in AAC_tactics.Instances]
Bool.aac_Bool_andb_Comm [instance, in AAC_tactics.Instances]
Bool.aac_Bool_andb_Assoc [instance, in AAC_tactics.Instances]
Bool.aac_Bool_orb_Idem [instance, in AAC_tactics.Instances]
Bool.aac_Bool_orb_Comm [instance, in AAC_tactics.Instances]
Bool.aac_Bool_orb_Assoc [instance, in AAC_tactics.Instances]
Bool.negb_compat [instance, in AAC_tactics.Instances]
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]
compare_weak_spec_sind [definition, in AAC_tactics.Utils]
compare_weak_spec_ind [definition, in AAC_tactics.Utils]
compare_weak_spec [inductive, in AAC_tactics.Utils]
cons [constructor, in AAC_tactics.Utils]
Constants [library]
D
decide_spec_sind [definition, in AAC_tactics.Utils]decide_spec_ind [definition, in AAC_tactics.Utils]
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]
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]
F
fold_map' [definition, in AAC_tactics.Utils]fold_map [definition, in AAC_tactics.Utils]
H
Hbin1 [lemma, in AAC_tactics.Tutorial]Hbin2 [lemma, in AAC_tactics.Tutorial]
Hopp [lemma, in AAC_tactics.Tutorial]
I
Idempotent [record, in AAC_tactics.AAC]Idempotent [inductive, in AAC_tactics.AAC]
idx [abbreviation, in AAC_tactics.Utils]
ineq [section, in AAC_tactics.Caveats]
ineq.H [variable, in AAC_tactics.Caveats]
insert [definition, 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.pack [record, in AAC_tactics.AAC]
Internal.Bin.t [section, in AAC_tactics.AAC]
Internal.Bin.t.R [variable, in AAC_tactics.AAC]
Internal.Bin.t.X [variable, 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_sind [definition, in AAC_tactics.AAC]
Internal.compat_prd_unit_ind [definition, 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_sind [definition, in AAC_tactics.AAC]
Internal.compat_sum_unit_ind [definition, 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.copy.HR [variable, in AAC_tactics.AAC]
Internal.copy.op [variable, in AAC_tactics.AAC]
Internal.copy.op' [variable, in AAC_tactics.AAC]
Internal.copy.plus [variable, in AAC_tactics.AAC]
Internal.copy.po [variable, in AAC_tactics.AAC]
Internal.copy.R [variable, in AAC_tactics.AAC]
Internal.copy.X [variable, 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.discr_sind [definition, in AAC_tactics.AAC]
Internal.discr_rec [definition, in AAC_tactics.AAC]
Internal.discr_ind [definition, in AAC_tactics.AAC]
Internal.discr_rect [definition, 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_ind_sind [definition, in AAC_tactics.AAC]
Internal.is_prd_spec_ind_ind [definition, 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_ind_sind [definition, in AAC_tactics.AAC]
Internal.is_sum_spec_ind_ind [definition, 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.m_sind [definition, in AAC_tactics.AAC]
Internal.m_rec [definition, in AAC_tactics.AAC]
Internal.m_ind [definition, in AAC_tactics.AAC]
Internal.m_rect [definition, 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.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.t.R [variable, in AAC_tactics.AAC]
Internal.Sym.t.X [variable, in AAC_tactics.AAC]
Internal.Sym.value [projection, in AAC_tactics.AAC]
Internal.s.E [variable, 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.R [variable, 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]
Internal.s.X [variable, 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.T_sind [definition, in AAC_tactics.AAC]
Internal.T_rec [definition, in AAC_tactics.AAC]
Internal.T_ind [definition, in AAC_tactics.AAC]
Internal.T_rect [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.vT_sind [definition, in AAC_tactics.AAC]
Internal.vT_rec [definition, in AAC_tactics.AAC]
Internal.vT_ind [definition, in AAC_tactics.AAC]
Internal.vT_rect [definition, 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]
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]
lists [section, in AAC_tactics.Utils]
Lists [module, in AAC_tactics.Instances]
Lists [section, in AAC_tactics.Tutorial]
Lists.aac_List_app_nil_Permutation_Unit [instance, in AAC_tactics.Instances]
Lists.aac_List_app_Permutation_Comm [instance, in AAC_tactics.Instances]
Lists.aac_List_app_Permutation_Assoc [instance, in AAC_tactics.Instances]
Lists.aac_List_app_nil_Unit [instance, in AAC_tactics.Instances]
Lists.aac_List_app_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]
M
merge_map [definition, in AAC_tactics.Utils]merge_msets [definition, in AAC_tactics.Utils]
morphism [section, in AAC_tactics.Caveats]
morphism.H [variable, in AAC_tactics.Caveats]
morphism.HP [variable, in AAC_tactics.Caveats]
morphism.P [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]
N
N [module, in AAC_tactics.Instances]nelist [inductive, in AAC_tactics.Utils]
nelist_map [definition, in AAC_tactics.Utils]
nelist_sind [definition, in AAC_tactics.Utils]
nelist_rec [definition, in AAC_tactics.Utils]
nelist_ind [definition, in AAC_tactics.Utils]
nelist_rect [definition, in AAC_tactics.Utils]
nil [constructor, in AAC_tactics.Utils]
N.aac_N_le_eq_lift [instance, in AAC_tactics.Instances]
N.aac_N_gcd_0_Unit [instance, in AAC_tactics.Instances]
N.aac_N_max_0_Unit [instance, in AAC_tactics.Instances]
N.aac_N_add_0_Unit [instance, in AAC_tactics.Instances]
N.aac_N_lcm_1_Unit [instance, in AAC_tactics.Instances]
N.aac_N_mul_1_Unit [instance, in AAC_tactics.Instances]
N.aac_N_lcm_Idem [instance, in AAC_tactics.Instances]
N.aac_N_lcm_Assoc [instance, in AAC_tactics.Instances]
N.aac_N_lcm_Comm [instance, in AAC_tactics.Instances]
N.aac_N_gcd_Idem [instance, in AAC_tactics.Instances]
N.aac_N_gcd_Assoc [instance, in AAC_tactics.Instances]
N.aac_N_gcd_Comm [instance, in AAC_tactics.Instances]
N.aac_N_max_Idem [instance, in AAC_tactics.Instances]
N.aac_N_max_Assoc [instance, in AAC_tactics.Instances]
N.aac_N_max_Comm [instance, in AAC_tactics.Instances]
N.aac_N_min_Idem [instance, in AAC_tactics.Instances]
N.aac_N_min_Assoc [instance, in AAC_tactics.Instances]
N.aac_N_min_Comm [instance, in AAC_tactics.Instances]
N.aac_N_mul_Assoc [instance, in AAC_tactics.Instances]
N.aac_N_mul_Comm [instance, in AAC_tactics.Instances]
N.aac_N_add_Comm [instance, in AAC_tactics.Instances]
N.aac_N_add_Assoc [instance, in AAC_tactics.Instances]
N.N_le_PreOrder [instance, in AAC_tactics.Instances]
P
P [module, in AAC_tactics.Instances]parameters [section, in AAC_tactics.Caveats]
parameters.E [variable, 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]
parameters.plus [variable, in AAC_tactics.Caveats]
parameters.plus_Proper [variable, in AAC_tactics.Caveats]
parameters.plus_C [variable, in AAC_tactics.Caveats]
parameters.plus_A [variable, in AAC_tactics.Caveats]
parameters.R [variable, in AAC_tactics.Caveats]
parameters.X [variable, in AAC_tactics.Caveats]
parameters.Zero [variable, in AAC_tactics.Caveats]
parameters.zero [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_Nat_le_eq_lift [instance, in AAC_tactics.Instances]
Peano.aac_Nat_gcd_0_Unit [instance, in AAC_tactics.Instances]
Peano.aac_Nat_max_0_Unit [instance, in AAC_tactics.Instances]
Peano.aac_Nat_add_0_Unit [instance, in AAC_tactics.Instances]
Peano.aac_Nat_lcm_1_Unit [instance, in AAC_tactics.Instances]
Peano.aac_Nat_mul_1_Unit [instance, in AAC_tactics.Instances]
Peano.aac_Nat_lcm_Idem [instance, in AAC_tactics.Instances]
Peano.aac_Nat_lcm_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_Nat_lcm_Comm [instance, in AAC_tactics.Instances]
Peano.aac_Nat_gcd_Idem [instance, in AAC_tactics.Instances]
Peano.aac_Nat_gcd_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_Nat_gcd_Comm [instance, in AAC_tactics.Instances]
Peano.aac_Nat_max_Idem [instance, in AAC_tactics.Instances]
Peano.aac_Nat_max_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_Nat_max_Comm [instance, in AAC_tactics.Instances]
Peano.aac_Nat_min_Idem [instance, in AAC_tactics.Instances]
Peano.aac_Nat_min_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_Nat_min_Comm [instance, in AAC_tactics.Instances]
Peano.aac_Nat_mul_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_Nat_mul_Comm [instance, in AAC_tactics.Instances]
Peano.aac_Nat_add_Comm [instance, in AAC_tactics.Instances]
Peano.aac_Nat_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.Nat_le_PreOrder [instance, in AAC_tactics.Instances]
pos_compare_reflect_eq [lemma, in AAC_tactics.Utils]
pos_compare_weak_spec [lemma, in AAC_tactics.Utils]
Props [section, in AAC_tactics.Tutorial]
Props.P [variable, in AAC_tactics.Tutorial]
Props.Q [variable, in AAC_tactics.Tutorial]
Prop_ops.aac_Prop_impl_iff_lift [instance, in AAC_tactics.Instances]
Prop_ops.not_iff_compat [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_True_iff_Unit [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_False_iff_Unit [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_iff_Idem [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_iff_Comm [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_iff_Assoc [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_iff_Idem [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_iff_Comm [instance, in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_iff_Assoc [instance, in AAC_tactics.Instances]
Prop_ops [module, in AAC_tactics.Instances]
P.aac_Pos_le_eq_lift [instance, in AAC_tactics.Instances]
P.aac_Pos_max_1_Unit [instance, in AAC_tactics.Instances]
P.aac_Pos_mul_1_Unit [instance, in AAC_tactics.Instances]
P.aac_Pos_max_Idem [instance, in AAC_tactics.Instances]
P.aac_Pos_max_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pos_max_Comm [instance, in AAC_tactics.Instances]
P.aac_Pos_min_Idem [instance, in AAC_tactics.Instances]
P.aac_Pos_min_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pos_min_Comm [instance, in AAC_tactics.Instances]
P.aac_Pos_mul_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pos_mul_Comm [instance, in AAC_tactics.Instances]
P.aac_Pos_add_Comm [instance, in AAC_tactics.Instances]
P.aac_Pos_add_Assoc [instance, in AAC_tactics.Instances]
P.Pos_le_PreOrder [instance, in AAC_tactics.Instances]
Q
Q [module, in AAC_tactics.Instances]Q.aac_Q_Qle_eq_lift [instance, in AAC_tactics.Instances]
Q.aac_Q_Qplus_0_Qeq_Unit [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmult_1_Qeq_Unit [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmax_Qeq_Idem [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmax_Qeq_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmax_Qeq_Comm [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmin_Qeq_Idem [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmin_Qeq_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmin_Qeq_Comm [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmult_Qeq_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Q_Qmult_Qeq_Comm [instance, in AAC_tactics.Instances]
Q.aac_Q_Qplus_Qeq_Comm [instance, in AAC_tactics.Instances]
Q.aac_Q_Qplus_Qeq_Assoc [instance, in AAC_tactics.Instances]
Q.Q_Qle_PreOrder [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_inclusion_same_relation_lift [instance, in AAC_tactics.Instances]
Relations.aac_compo_eq_same_relation_Unit [instance, in AAC_tactics.Instances]
Relations.aac_compo_same_relation_Assoc [instance, in AAC_tactics.Instances]
Relations.aac_inter_top_same_relation_Unit [instance, in AAC_tactics.Instances]
Relations.aac_inter_same_relation_Idem [instance, in AAC_tactics.Instances]
Relations.aac_inter_same_relation_Assoc [instance, in AAC_tactics.Instances]
Relations.aac_inter_same_relation_Comm [instance, in AAC_tactics.Instances]
Relations.aac_bot_union_same_relation_Unit [instance, in AAC_tactics.Instances]
Relations.aac_union_same_relation_Idem [instance, in AAC_tactics.Instances]
Relations.aac_union_same_relation_Assoc [instance, in AAC_tactics.Instances]
Relations.aac_union_same_relation_Comm [instance, in AAC_tactics.Instances]
Relations.bot [definition, in AAC_tactics.Instances]
Relations.clos_refl_trans_same_relation_compat [instance, in AAC_tactics.Instances]
Relations.clos_refl_trans_incr [instance, in AAC_tactics.Instances]
Relations.clos_trans_same_relation_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.inclusion_PreOrder [instance, in AAC_tactics.Instances]
Relations.inter [definition, in AAC_tactics.Instances]
Relations.negr [definition, in AAC_tactics.Instances]
Relations.negr_same_relation_compat [instance, in AAC_tactics.Instances]
Relations.same_relation_Equivalence [instance, in AAC_tactics.Instances]
Relations.top [definition, in AAC_tactics.Instances]
Relations.transp_same_relation_compat [instance, in AAC_tactics.Instances]
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]
T
t [section, in AAC_tactics.AAC]transitivity4 [lemma, in AAC_tactics.AAC]
Tutorial [library]
U
U [section, in AAC_tactics.Caveats]Unit [record, 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_thm29 [definition, in AAC_tactics.Tutorial]
Unnamed_thm28 [definition, in AAC_tactics.Tutorial]
Unnamed_thm27 [definition, in AAC_tactics.Tutorial]
Unnamed_thm26 [definition, in AAC_tactics.Tutorial]
Unnamed_thm25 [definition, in AAC_tactics.Tutorial]
Unnamed_thm24 [definition, in AAC_tactics.Tutorial]
Unnamed_thm23 [definition, in AAC_tactics.Tutorial]
Unnamed_thm22 [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_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]
Utils [library]
U.dot [variable, in AAC_tactics.Caveats]
U.dot_inv_right [variable, in AAC_tactics.Caveats]
U.dot_inv_left [variable, in AAC_tactics.Caveats]
U.dot_Proper [variable, in AAC_tactics.Caveats]
U.dot_A [variable, in AAC_tactics.Caveats]
U.E [variable, in AAC_tactics.Caveats]
U.f [variable, in AAC_tactics.Caveats]
U.Hf [variable, in AAC_tactics.Caveats]
U.One [variable, in AAC_tactics.Caveats]
U.one [variable, in AAC_tactics.Caveats]
U.R [variable, in AAC_tactics.Caveats]
U.X [variable, in AAC_tactics.Caveats]
_ * _ [notation, in AAC_tactics.Caveats]
_ == _ [notation, in AAC_tactics.Caveats]
1 [notation, in AAC_tactics.Caveats]
V
V [section, in AAC_tactics.Caveats]V.dot [variable, in AAC_tactics.Caveats]
V.dot_Proper [variable, in AAC_tactics.Caveats]
V.dot_A [variable, in AAC_tactics.Caveats]
V.E [variable, in AAC_tactics.Caveats]
V.One [variable, in AAC_tactics.Caveats]
V.one [variable, in AAC_tactics.Caveats]
V.R [variable, in AAC_tactics.Caveats]
V.X [variable, in AAC_tactics.Caveats]
_ * _ [notation, in AAC_tactics.Caveats]
_ == _ [notation, in AAC_tactics.Caveats]
1 [notation, in AAC_tactics.Caveats]
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]
Z
Z [section, in AAC_tactics.Caveats]Z [module, in AAC_tactics.Instances]
Z_add_incr [instance, in AAC_tactics.Caveats]
Z_add_le_compat [instance, in AAC_tactics.Tutorial]
Z_opp_ge_le_compat [instance, in AAC_tactics.Tutorial]
Z_add_opp_diag_r [lemma, in AAC_tactics.Tutorial]
Z_abs_triangle [lemma, in AAC_tactics.Tutorial]
Z.a [variable, in AAC_tactics.Caveats]
Z.aac_Z_le_eq_lift [instance, in AAC_tactics.Instances]
Z.aac_Z_add_0_Unit [instance, in AAC_tactics.Instances]
Z.aac_Z_mul_1_Unit [instance, in AAC_tactics.Instances]
Z.aac_Z_lcm_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Z_lcm_Comm [instance, in AAC_tactics.Instances]
Z.aac_Z_gcd_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Z_gcd_Comm [instance, in AAC_tactics.Instances]
Z.aac_Z_max_Idem [instance, in AAC_tactics.Instances]
Z.aac_Z_max_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Z_max_Comm [instance, in AAC_tactics.Instances]
Z.aac_Z_min_Idem [instance, in AAC_tactics.Instances]
Z.aac_Z_min_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Z_min_Comm [instance, in AAC_tactics.Instances]
Z.aac_Z_mul_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Z_mul_Comm [instance, in AAC_tactics.Instances]
Z.aac_Z_add_Comm [instance, in AAC_tactics.Instances]
Z.aac_Z_add_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.Z_le_PreOrder [instance, in AAC_tactics.Instances]
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]
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.dot [in AAC_tactics.Tutorial]
base.dot_Proper [in AAC_tactics.Tutorial]
base.dot_A [in AAC_tactics.Tutorial]
base.E [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.One [in AAC_tactics.Tutorial]
base.one [in AAC_tactics.Tutorial]
base.plus [in AAC_tactics.Tutorial]
base.plus_Proper [in AAC_tactics.Tutorial]
base.plus_C [in AAC_tactics.Tutorial]
base.plus_A [in AAC_tactics.Tutorial]
base.R [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]
base.X [in AAC_tactics.Tutorial]
base.Zero [in AAC_tactics.Tutorial]
base.zero [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.Bin.t.R [in AAC_tactics.AAC]
Internal.Bin.t.X [in AAC_tactics.AAC]
Internal.copy.HR [in AAC_tactics.AAC]
Internal.copy.op [in AAC_tactics.AAC]
Internal.copy.op' [in AAC_tactics.AAC]
Internal.copy.plus [in AAC_tactics.AAC]
Internal.copy.po [in AAC_tactics.AAC]
Internal.copy.R [in AAC_tactics.AAC]
Internal.copy.X [in AAC_tactics.AAC]
Internal.Sym.t.R [in AAC_tactics.AAC]
Internal.Sym.t.X [in AAC_tactics.AAC]
Internal.s.E [in AAC_tactics.AAC]
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.R [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]
Internal.s.X [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]morphism.HP [in AAC_tactics.Caveats]
morphism.P [in AAC_tactics.Caveats]
P
parameters.E [in AAC_tactics.Caveats]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]
parameters.plus [in AAC_tactics.Caveats]
parameters.plus_Proper [in AAC_tactics.Caveats]
parameters.plus_C [in AAC_tactics.Caveats]
parameters.plus_A [in AAC_tactics.Caveats]
parameters.R [in AAC_tactics.Caveats]
parameters.X [in AAC_tactics.Caveats]
parameters.Zero [in AAC_tactics.Caveats]
parameters.zero [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]
Props.P [in AAC_tactics.Tutorial]
Props.Q [in AAC_tactics.Tutorial]
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 [in AAC_tactics.Caveats]U.dot_inv_right [in AAC_tactics.Caveats]
U.dot_inv_left [in AAC_tactics.Caveats]
U.dot_Proper [in AAC_tactics.Caveats]
U.dot_A [in AAC_tactics.Caveats]
U.E [in AAC_tactics.Caveats]
U.f [in AAC_tactics.Caveats]
U.Hf [in AAC_tactics.Caveats]
U.One [in AAC_tactics.Caveats]
U.one [in AAC_tactics.Caveats]
U.R [in AAC_tactics.Caveats]
U.X [in AAC_tactics.Caveats]
V
V.dot [in AAC_tactics.Caveats]V.dot_Proper [in AAC_tactics.Caveats]
V.dot_A [in AAC_tactics.Caveats]
V.E [in AAC_tactics.Caveats]
V.One [in AAC_tactics.Caveats]
V.one [in AAC_tactics.Caveats]
V.R [in AAC_tactics.Caveats]
V.X [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
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_reflect_eq [in AAC_tactics.Utils]pos_compare_weak_spec [in AAC_tactics.Utils]
R
reflect_eqdep_weak_spec [in AAC_tactics.Utils]reflect_eqdep_eq [in AAC_tactics.Utils]
T
transitivity4 [in AAC_tactics.AAC]Z
Z_add_opp_diag_r [in AAC_tactics.Tutorial]Z_abs_triangle [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.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.prd [in AAC_tactics.AAC]
Internal.right [in AAC_tactics.AAC]
Internal.sum [in AAC_tactics.AAC]
Internal.sym [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]
Props [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_le_eq_lift [in AAC_tactics.Tutorial]
aac_Nat_max_0_Unit [in AAC_tactics.Tutorial]
aac_Nat_max_Idem [in AAC_tactics.Tutorial]
aac_Nat_max_Assoc [in AAC_tactics.Tutorial]
aac_Nat_max_Comm [in AAC_tactics.Tutorial]
aac_Nat_add_0_Unit [in AAC_tactics.Tutorial]
aac_Nat_mul_1_Unit [in AAC_tactics.Tutorial]
aac_Nat_mul_Assoc [in AAC_tactics.Tutorial]
aac_Nat_mul_Comm [in AAC_tactics.Tutorial]
aac_Nat_add_Comm [in AAC_tactics.Tutorial]
aac_Nat_add_Assoc [in AAC_tactics.Tutorial]
B
Bool.aac_Bool_andb_true_Unit [in AAC_tactics.Instances]Bool.aac_Bool_orb_false_Unit [in AAC_tactics.Instances]
Bool.aac_Bool_andb_Idem [in AAC_tactics.Instances]
Bool.aac_Bool_andb_Comm [in AAC_tactics.Instances]
Bool.aac_Bool_andb_Assoc [in AAC_tactics.Instances]
Bool.aac_Bool_orb_Idem [in AAC_tactics.Instances]
Bool.aac_Bool_orb_Comm [in AAC_tactics.Instances]
Bool.aac_Bool_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
Lists.aac_List_app_nil_Permutation_Unit [in AAC_tactics.Instances]Lists.aac_List_app_Permutation_Comm [in AAC_tactics.Instances]
Lists.aac_List_app_Permutation_Assoc [in AAC_tactics.Instances]
Lists.aac_List_app_nil_Unit [in AAC_tactics.Instances]
Lists.aac_List_app_Assoc [in AAC_tactics.Instances]
N
N.aac_N_le_eq_lift [in AAC_tactics.Instances]N.aac_N_gcd_0_Unit [in AAC_tactics.Instances]
N.aac_N_max_0_Unit [in AAC_tactics.Instances]
N.aac_N_add_0_Unit [in AAC_tactics.Instances]
N.aac_N_lcm_1_Unit [in AAC_tactics.Instances]
N.aac_N_mul_1_Unit [in AAC_tactics.Instances]
N.aac_N_lcm_Idem [in AAC_tactics.Instances]
N.aac_N_lcm_Assoc [in AAC_tactics.Instances]
N.aac_N_lcm_Comm [in AAC_tactics.Instances]
N.aac_N_gcd_Idem [in AAC_tactics.Instances]
N.aac_N_gcd_Assoc [in AAC_tactics.Instances]
N.aac_N_gcd_Comm [in AAC_tactics.Instances]
N.aac_N_max_Idem [in AAC_tactics.Instances]
N.aac_N_max_Assoc [in AAC_tactics.Instances]
N.aac_N_max_Comm [in AAC_tactics.Instances]
N.aac_N_min_Idem [in AAC_tactics.Instances]
N.aac_N_min_Assoc [in AAC_tactics.Instances]
N.aac_N_min_Comm [in AAC_tactics.Instances]
N.aac_N_mul_Assoc [in AAC_tactics.Instances]
N.aac_N_mul_Comm [in AAC_tactics.Instances]
N.aac_N_add_Comm [in AAC_tactics.Instances]
N.aac_N_add_Assoc [in AAC_tactics.Instances]
N.N_le_PreOrder [in AAC_tactics.Instances]
P
Peano.aac_Nat_le_eq_lift [in AAC_tactics.Instances]Peano.aac_Nat_gcd_0_Unit [in AAC_tactics.Instances]
Peano.aac_Nat_max_0_Unit [in AAC_tactics.Instances]
Peano.aac_Nat_add_0_Unit [in AAC_tactics.Instances]
Peano.aac_Nat_lcm_1_Unit [in AAC_tactics.Instances]
Peano.aac_Nat_mul_1_Unit [in AAC_tactics.Instances]
Peano.aac_Nat_lcm_Idem [in AAC_tactics.Instances]
Peano.aac_Nat_lcm_Assoc [in AAC_tactics.Instances]
Peano.aac_Nat_lcm_Comm [in AAC_tactics.Instances]
Peano.aac_Nat_gcd_Idem [in AAC_tactics.Instances]
Peano.aac_Nat_gcd_Assoc [in AAC_tactics.Instances]
Peano.aac_Nat_gcd_Comm [in AAC_tactics.Instances]
Peano.aac_Nat_max_Idem [in AAC_tactics.Instances]
Peano.aac_Nat_max_Assoc [in AAC_tactics.Instances]
Peano.aac_Nat_max_Comm [in AAC_tactics.Instances]
Peano.aac_Nat_min_Idem [in AAC_tactics.Instances]
Peano.aac_Nat_min_Assoc [in AAC_tactics.Instances]
Peano.aac_Nat_min_Comm [in AAC_tactics.Instances]
Peano.aac_Nat_mul_Assoc [in AAC_tactics.Instances]
Peano.aac_Nat_mul_Comm [in AAC_tactics.Instances]
Peano.aac_Nat_add_Comm [in AAC_tactics.Instances]
Peano.aac_Nat_add_Assoc [in AAC_tactics.Instances]
Peano.Nat_le_PreOrder [in AAC_tactics.Instances]
Prop_ops.aac_Prop_impl_iff_lift [in AAC_tactics.Instances]
Prop_ops.not_iff_compat [in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_True_iff_Unit [in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_False_iff_Unit [in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_iff_Idem [in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_iff_Comm [in AAC_tactics.Instances]
Prop_ops.aac_Prop_and_iff_Assoc [in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_iff_Idem [in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_iff_Comm [in AAC_tactics.Instances]
Prop_ops.aac_Prop_or_iff_Assoc [in AAC_tactics.Instances]
P.aac_Pos_le_eq_lift [in AAC_tactics.Instances]
P.aac_Pos_max_1_Unit [in AAC_tactics.Instances]
P.aac_Pos_mul_1_Unit [in AAC_tactics.Instances]
P.aac_Pos_max_Idem [in AAC_tactics.Instances]
P.aac_Pos_max_Assoc [in AAC_tactics.Instances]
P.aac_Pos_max_Comm [in AAC_tactics.Instances]
P.aac_Pos_min_Idem [in AAC_tactics.Instances]
P.aac_Pos_min_Assoc [in AAC_tactics.Instances]
P.aac_Pos_min_Comm [in AAC_tactics.Instances]
P.aac_Pos_mul_Assoc [in AAC_tactics.Instances]
P.aac_Pos_mul_Comm [in AAC_tactics.Instances]
P.aac_Pos_add_Comm [in AAC_tactics.Instances]
P.aac_Pos_add_Assoc [in AAC_tactics.Instances]
P.Pos_le_PreOrder [in AAC_tactics.Instances]
Q
Q.aac_Q_Qle_eq_lift [in AAC_tactics.Instances]Q.aac_Q_Qplus_0_Qeq_Unit [in AAC_tactics.Instances]
Q.aac_Q_Qmult_1_Qeq_Unit [in AAC_tactics.Instances]
Q.aac_Q_Qmax_Qeq_Idem [in AAC_tactics.Instances]
Q.aac_Q_Qmax_Qeq_Assoc [in AAC_tactics.Instances]
Q.aac_Q_Qmax_Qeq_Comm [in AAC_tactics.Instances]
Q.aac_Q_Qmin_Qeq_Idem [in AAC_tactics.Instances]
Q.aac_Q_Qmin_Qeq_Assoc [in AAC_tactics.Instances]
Q.aac_Q_Qmin_Qeq_Comm [in AAC_tactics.Instances]
Q.aac_Q_Qmult_Qeq_Assoc [in AAC_tactics.Instances]
Q.aac_Q_Qmult_Qeq_Comm [in AAC_tactics.Instances]
Q.aac_Q_Qplus_Qeq_Comm [in AAC_tactics.Instances]
Q.aac_Q_Qplus_Qeq_Assoc [in AAC_tactics.Instances]
Q.Q_Qle_PreOrder [in AAC_tactics.Instances]
R
Relations.aac_inclusion_same_relation_lift [in AAC_tactics.Instances]Relations.aac_compo_eq_same_relation_Unit [in AAC_tactics.Instances]
Relations.aac_compo_same_relation_Assoc [in AAC_tactics.Instances]
Relations.aac_inter_top_same_relation_Unit [in AAC_tactics.Instances]
Relations.aac_inter_same_relation_Idem [in AAC_tactics.Instances]
Relations.aac_inter_same_relation_Assoc [in AAC_tactics.Instances]
Relations.aac_inter_same_relation_Comm [in AAC_tactics.Instances]
Relations.aac_bot_union_same_relation_Unit [in AAC_tactics.Instances]
Relations.aac_union_same_relation_Idem [in AAC_tactics.Instances]
Relations.aac_union_same_relation_Assoc [in AAC_tactics.Instances]
Relations.aac_union_same_relation_Comm [in AAC_tactics.Instances]
Relations.clos_refl_trans_same_relation_compat [in AAC_tactics.Instances]
Relations.clos_refl_trans_incr [in AAC_tactics.Instances]
Relations.clos_trans_same_relation_compat [in AAC_tactics.Instances]
Relations.clos_trans_incr [in AAC_tactics.Instances]
Relations.inclusion_PreOrder [in AAC_tactics.Instances]
Relations.negr_same_relation_compat [in AAC_tactics.Instances]
Relations.same_relation_Equivalence [in AAC_tactics.Instances]
Relations.transp_same_relation_compat [in AAC_tactics.Instances]
Z
Z_add_incr [in AAC_tactics.Caveats]Z_add_le_compat [in AAC_tactics.Tutorial]
Z_opp_ge_le_compat [in AAC_tactics.Tutorial]
Z.aac_Z_le_eq_lift [in AAC_tactics.Instances]
Z.aac_Z_add_0_Unit [in AAC_tactics.Instances]
Z.aac_Z_mul_1_Unit [in AAC_tactics.Instances]
Z.aac_Z_lcm_Assoc [in AAC_tactics.Instances]
Z.aac_Z_lcm_Comm [in AAC_tactics.Instances]
Z.aac_Z_gcd_Assoc [in AAC_tactics.Instances]
Z.aac_Z_gcd_Comm [in AAC_tactics.Instances]
Z.aac_Z_max_Idem [in AAC_tactics.Instances]
Z.aac_Z_max_Assoc [in AAC_tactics.Instances]
Z.aac_Z_max_Comm [in AAC_tactics.Instances]
Z.aac_Z_min_Idem [in AAC_tactics.Instances]
Z.aac_Z_min_Assoc [in AAC_tactics.Instances]
Z.aac_Z_min_Comm [in AAC_tactics.Instances]
Z.aac_Z_mul_Assoc [in AAC_tactics.Instances]
Z.aac_Z_mul_Comm [in AAC_tactics.Instances]
Z.aac_Z_add_Comm [in AAC_tactics.Instances]
Z.aac_Z_add_Assoc [in AAC_tactics.Instances]
Z.Z_le_PreOrder [in AAC_tactics.Instances]
Abbreviation Index
C
cast [in AAC_tactics.Utils]I
idx [in AAC_tactics.Utils]L
lex [in AAC_tactics.Utils]Definition Index
A
appne [in AAC_tactics.Utils]C
compare_weak_spec_sind [in AAC_tactics.Utils]compare_weak_spec_ind [in AAC_tactics.Utils]
D
decide_spec_sind [in AAC_tactics.Utils]decide_spec_ind [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
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.compat_prd_unit_sind [in AAC_tactics.AAC]
Internal.compat_prd_unit_ind [in AAC_tactics.AAC]
Internal.compat_sum_unit_sind [in AAC_tactics.AAC]
Internal.compat_sum_unit_ind [in AAC_tactics.AAC]
Internal.copy [in AAC_tactics.AAC]
Internal.copy_mset [in AAC_tactics.AAC]
Internal.copy' [in AAC_tactics.AAC]
Internal.discr_sind [in AAC_tactics.AAC]
Internal.discr_rec [in AAC_tactics.AAC]
Internal.discr_ind [in AAC_tactics.AAC]
Internal.discr_rect [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_spec_ind_sind [in AAC_tactics.AAC]
Internal.is_prd_spec_ind_ind [in AAC_tactics.AAC]
Internal.is_sum_spec_ind_sind [in AAC_tactics.AAC]
Internal.is_sum_spec_ind_ind [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.m_sind [in AAC_tactics.AAC]
Internal.m_rec [in AAC_tactics.AAC]
Internal.m_ind [in AAC_tactics.AAC]
Internal.m_rect [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.T_sind [in AAC_tactics.AAC]
Internal.T_rec [in AAC_tactics.AAC]
Internal.T_ind [in AAC_tactics.AAC]
Internal.T_rect [in AAC_tactics.AAC]
Internal.vcompare [in AAC_tactics.AAC]
Internal.vcompare_reflect_eqdep [in AAC_tactics.AAC]
Internal.vnorm [in AAC_tactics.AAC]
Internal.vT_sind [in AAC_tactics.AAC]
Internal.vT_rec [in AAC_tactics.AAC]
Internal.vT_ind [in AAC_tactics.AAC]
Internal.vT_rect [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]nelist_sind [in AAC_tactics.Utils]
nelist_rec [in AAC_tactics.Utils]
nelist_ind [in AAC_tactics.Utils]
nelist_rect [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_thm29 [in AAC_tactics.Tutorial]
Unnamed_thm28 [in AAC_tactics.Tutorial]
Unnamed_thm27 [in AAC_tactics.Tutorial]
Unnamed_thm26 [in AAC_tactics.Tutorial]
Unnamed_thm25 [in AAC_tactics.Tutorial]
Unnamed_thm24 [in AAC_tactics.Tutorial]
Unnamed_thm23 [in AAC_tactics.Tutorial]
Unnamed_thm22 [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_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 | (685 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) |
| 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 | (176 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 | (31 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 | (39 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 | (161 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 | (3 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 | (140 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) |