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 (490 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 (114 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 (5 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 (56 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 (34 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 (13 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 (17 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 (37 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 (119 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 (51 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 (8 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_Assoc [instance, in AAC_tactics.Tutorial]
aac_max_Comm [instance, in AAC_tactics.Tutorial]
aac_zero_plus [instance, in AAC_tactics.Tutorial]
aac_one [instance, in AAC_tactics.Tutorial]
aac_plus_Comm [instance, in AAC_tactics.Tutorial]
aac_plus_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.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_Comm [instance, in AAC_tactics.Instances]
Bool.aac_andb_Assoc [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]


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 [inductive, in AAC_tactics.Utils]
cons [constructor, in AAC_tactics.Utils]


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]


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

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]
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_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.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_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 [lemma, in AAC_tactics.AAC]
Internal.eval_norm [lemma, 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_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_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 [lemma, 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 [lemma, 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]


L

law_neutral_right [projection, in AAC_tactics.AAC]
law_neutral_left [projection, 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.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.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.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]
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]
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]
nil [constructor, in AAC_tactics.Utils]
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_Assoc [instance, in AAC_tactics.Instances]
N.aac_Nmax_Comm [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]


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.Tutorial]
Peano [section, in AAC_tactics.Caveats]
Peano [module, in AAC_tactics.Instances]
Peano.a [variable, in AAC_tactics.Tutorial]
Peano.aac_zero_max [instance, in AAC_tactics.Instances]
Peano.aac_zero_plus [instance, in AAC_tactics.Instances]
Peano.aac_one [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_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_min_Comm [instance, in AAC_tactics.Instances]
Peano.aac_mult_Assoc [instance, in AAC_tactics.Instances]
Peano.aac_mult_Comm [instance, in AAC_tactics.Instances]
Peano.aac_plus_Comm [instance, in AAC_tactics.Instances]
Peano.aac_plus_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.Tutorial]
Peano.H [variable, in AAC_tactics.Caveats]
Peano.H' [variable, in AAC_tactics.Caveats]
Peano.lift_le_eq [instance, in AAC_tactics.Instances]
Peano.preorder_le [instance, in AAC_tactics.Instances]
pos_compare_weak_spec [lemma, in AAC_tactics.Utils]
pos_compare [abbreviation, in AAC_tactics.Utils]
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_Comm [instance, in AAC_tactics.Instances]
Prop_ops.aac_and_Assoc [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_Assoc [instance, in AAC_tactics.Instances]
P.aac_Pmax_Comm [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.preorder_le [instance, in AAC_tactics.Instances]


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_Assoc [instance, in AAC_tactics.Instances]
Q.aac_Qmax_Comm [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

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


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]
Tutorial [library]


U

U [section, in AAC_tactics.Caveats]
Unit [record, 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]


V

V [section, 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]
Zabs_triangle [lemma, in AAC_tactics.Tutorial]
Zminus_compat [instance, in AAC_tactics.Tutorial]
Zplus_opp_r [lemma, in AAC_tactics.Tutorial]
Zplus_incr [instance, in AAC_tactics.Caveats]
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_Assoc [instance, in AAC_tactics.Instances]
Z.aac_Zmax_Comm [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]


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


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.Tutorial]
Peano.H [in AAC_tactics.Caveats]
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

AAC


C

Caveats


I

Instances


T

Tutorial


U

Utils



Lemma 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_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_aux [in AAC_tactics.AAC]
Internal.eval_norm [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_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.tcompare_weak_spec [in AAC_tactics.AAC]
Internal.vcompare_reflect_eqdep [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]


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

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.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_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.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.Tutorial]
Peano [in AAC_tactics.Caveats]


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_Assoc [in AAC_tactics.Tutorial]
aac_max_Comm [in AAC_tactics.Tutorial]
aac_zero_plus [in AAC_tactics.Tutorial]
aac_one [in AAC_tactics.Tutorial]
aac_plus_Comm [in AAC_tactics.Tutorial]
aac_plus_Assoc [in AAC_tactics.Tutorial]


B

Bool.aac_false [in AAC_tactics.Instances]
Bool.aac_true [in AAC_tactics.Instances]
Bool.aac_andb_Comm [in AAC_tactics.Instances]
Bool.aac_andb_Assoc [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_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_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_Assoc [in AAC_tactics.Instances]
N.aac_Nmax_Comm [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_plus [in AAC_tactics.Instances]
Peano.aac_one [in AAC_tactics.Instances]
Peano.aac_max_Assoc [in AAC_tactics.Instances]
Peano.aac_max_Comm [in AAC_tactics.Instances]
Peano.aac_min_Assoc [in AAC_tactics.Instances]
Peano.aac_min_Comm [in AAC_tactics.Instances]
Peano.aac_mult_Assoc [in AAC_tactics.Instances]
Peano.aac_mult_Comm [in AAC_tactics.Instances]
Peano.aac_plus_Comm [in AAC_tactics.Instances]
Peano.aac_plus_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_Comm [in AAC_tactics.Instances]
Prop_ops.aac_and_Assoc [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_Assoc [in AAC_tactics.Instances]
P.aac_Pmax_Comm [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_Assoc [in AAC_tactics.Instances]
Q.aac_Qmax_Comm [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_Assoc [in AAC_tactics.Instances]
Relations.aac_inter_Comm [in AAC_tactics.Instances]
Relations.aac_bot [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_Assoc [in AAC_tactics.Instances]
Z.aac_Zmax_Comm [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_aux [in AAC_tactics.AAC]
Internal.is_prd [in AAC_tactics.AAC]
Internal.is_sum [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.vcompare [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

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]



Record Index

A

AAC_lift [in AAC_tactics.AAC]
Associative [in AAC_tactics.AAC]


C

Commutative [in AAC_tactics.AAC]


I

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 (490 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 (114 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 (5 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 (56 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 (34 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 (13 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 (17 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 (37 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 (119 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 (51 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 (8 entries)

This page has been generated by coqdoc