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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 entries)
Axiom 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)

O

O [constructor, in O]
obligation [definition, in obligation]
ObsoletePmultNat [section, in ObsoletePmultNat]
odd [definition, in odd]
odd [inductive, in odd]
Odd [definition, in Odd]
odd_plus_odd_inv_l [lemma, in odd_plus_odd_inv_l]
odd_even_lem [lemma, in odd_even_lem]
odd_plus_even_inv_r [lemma, in odd_plus_even_inv_r]
odd_mult [lemma, in odd_mult]
odd_S [constructor, in odd_S]
odd_plus_r [lemma, in odd_plus_r]
odd_spec [lemma, in odd_spec]
odd_mult_inv_l [lemma, in odd_mult_inv_l]
odd_S2n [lemma, in odd_S2n]
odd_plus_even_inv_l [lemma, in odd_plus_even_inv_l]
odd_plus_odd_inv_r [lemma, in odd_plus_odd_inv_r]
odd_even_plus [lemma, in odd_even_plus]
Odd_equiv [lemma, in Odd_equiv]
odd_mult_inv_r [lemma, in odd_mult_inv_r]
odd_div2 [lemma, in odd_div2]
odd_plus_split [lemma, in odd_plus_split]
odd_double [lemma, in odd_double]
odd_bitwise [lemma, in odd_bitwise]
odd_plus_l [lemma, in odd_plus_l]
OEQ [constructor, in OEQ]
of_nat [definition, in of_nat]
of_list [definition, in of_list]
of_nat_to_nat_inv [lemma, in of_nat_to_nat_inv]
of_pos [definition, in of_pos]
of_nat_lt [definition, in of_nat_lt]
OLE [constructor, in OLE]
OLT [constructor, in OLT]
Omega [lemma, in Omega]
OmniscientFunctionalChoice [abbreviation, in OmniscientFunctionalChoice]
OmniscientFunctionalChoice_on [definition, in OmniscientFunctionalChoice_on]
OmniscientRelationalChoice [abbreviation, in OmniscientRelationalChoice]
OmniscientRelationalChoice_on [definition, in OmniscientRelationalChoice_on]
omniscient_fun_choice_imp_fun_choice [lemma, in omniscient_fun_choice_imp_fun_choice]
omniscient_fun_choice_imp_small_drinker [lemma, in omniscient_fun_choice_imp_small_drinker]
On [definition, in On]
one [definition, in one]
one [definition, in one]
OneTwo [module, in OneTwo]
OneTwoNotation [module, in OneTwoNotation]
1 [notation, in ::'1']
2 [notation, in ::'2']
OneTwo' [module, in OneTwo']
OneTwo.one [axiom, in one]
OneTwo.two [axiom, in two]
one_IZR_r_R1 [lemma, in one_IZR_r_R1]
one_IZR_lt1 [lemma, in one_IZR_lt1]
open_set_P2 [lemma, in open_set_P2]
open_set_P6 [lemma, in open_set_P6]
open_set_P4 [lemma, in open_set_P4]
open_set_P5 [lemma, in open_set_P5]
open_set_P1 [lemma, in open_set_P1]
open_interval [definition, in open_interval]
open_set_P3 [lemma, in open_set_P3]
open_set [definition, in open_set]
Operators_Properties [library]
opp [definition, in opp]
Opp [module, in Opp]
OppCstNotation [module, in OppCstNotation]
- 2 [notation, in ::'-'_'2']
- 1 [notation, in ::'-'_'1']
OppNotation [module, in OppNotation]
- _ [notation, in ::'-'_x]
opp_carry [definition, in opp_carry]
opp_seq [definition, in opp_seq]
opp_fct [definition, in opp_fct]
opp_c [definition, in opp_c]
opp_IZR [lemma, in opp_IZR]
Opp' [module, in Opp']
Opp.opp [axiom, in opp]
opp31 [definition, in opp31]
Ops [module, in Ops]
Ops [module, in Ops]
Ops [module, in Ops]
Ops [module, in Ops]
Ops [module, in Ops]
Ops [module, in Ops]
Ops.add [definition, in add]
Ops.add [definition, in add]
Ops.add [definition, in add]
Ops.add [definition, in add]
Ops.append [definition, in append]
Ops.assert_false [definition, in assert_false]
Ops.bal [definition, in bal]
Ops.Bk [abbreviation, in Bk]
Ops.bogus [definition, in bogus]
Ops.cardinal [definition, in cardinal]
Ops.cardinal [definition, in cardinal]
Ops.cardinal [definition, in cardinal]
Ops.choose [definition, in choose]
Ops.choose [definition, in choose]
Ops.choose [definition, in choose]
Ops.compare [definition, in compare]
Ops.compare [definition, in compare]
Ops.compare_cont [definition, in compare_cont]
Ops.compare_height [definition, in compare_height]
Ops.compare_more [definition, in compare_more]
Ops.compare_end [definition, in compare_end]
Ops.concat [definition, in concat]
Ops.cons [definition, in cons]
Ops.create [definition, in create]
Ops.del [definition, in del]
Ops.delmin [definition, in delmin]
Ops.diff [definition, in diff]
Ops.diff [definition, in diff]
Ops.diff [definition, in diff]
Ops.diff [definition, in diff]
Ops.diff_list [definition, in diff_list]
Ops.elements [definition, in elements]
Ops.elements [definition, in elements]
Ops.elements [definition, in elements]
Ops.elements_aux [definition, in elements_aux]
Ops.elt [definition, in elt]
Ops.elt [definition, in elt]
Ops.elt [definition, in elt]
Ops.empty [definition, in empty]
Ops.empty [definition, in empty]
Ops.empty [definition, in empty]
Ops.End [constructor, in End]
Ops.enumeration [inductive, in enumeration]
Ops.equal [definition, in equal]
Ops.equal [definition, in equal]
Ops.equal [definition, in equal]
Ops.exists_ [definition, in exists_]
Ops.exists_ [definition, in exists_]
Ops.exists_ [definition, in exists_]
Ops.filter [definition, in filter]
Ops.filter [definition, in filter]
Ops.filter [definition, in filter]
Ops.filter [definition, in filter]
Ops.filter_aux [definition, in filter_aux]
Ops.fold [definition, in fold]
Ops.fold [definition, in fold]
Ops.fold [definition, in fold]
Ops.for_all [definition, in for_all]
Ops.for_all [definition, in for_all]
Ops.for_all [definition, in for_all]
Ops.height [definition, in height]
Ops.ins [definition, in ins]
Ops.inter [definition, in inter]
Ops.inter [definition, in inter]
Ops.inter [definition, in inter]
Ops.inter [definition, in inter]
Ops.inter_list [definition, in inter_list]
Ops.is_empty [definition, in is_empty]
Ops.is_empty [definition, in is_empty]
Ops.is_empty [definition, in is_empty]
Ops.join [definition, in join]
Ops.lbal [definition, in lbal]
Ops.lbalS [definition, in lbalS]
Ops.Leaf [constructor, in Leaf]
Ops.linear_diff [definition, in linear_diff]
Ops.linear_inter [definition, in linear_inter]
Ops.linear_union [definition, in linear_union]
Ops.makeBlack [definition, in makeBlack]
Ops.makeRed [definition, in makeRed]
Ops.maxdepth [definition, in maxdepth]
Ops.max_elt [definition, in max_elt]
Ops.max_elt [definition, in max_elt]
Ops.mem [definition, in mem]
Ops.mem [definition, in mem]
Ops.mem [definition, in mem]
Ops.merge [definition, in merge]
Ops.mindepth [definition, in mindepth]
Ops.min_elt [definition, in min_elt]
Ops.min_elt [definition, in min_elt]
Ops.mktriple [constructor, in mktriple]
Ops.More [constructor, in More]
Ops.Node [constructor, in Node]
Ops.partition [definition, in partition]
Ops.partition [definition, in partition]
Ops.partition [definition, in partition]
Ops.partition [definition, in partition]
Ops.partition_aux [definition, in partition_aux]
Ops.plength [definition, in plength]
Ops.plength_aux [definition, in plength_aux]
Ops.rbal [definition, in rbal]
Ops.rbalS [definition, in rbalS]
Ops.rbal' [definition, in rbal']
Ops.Rd [abbreviation, in Rd]
Ops.remove [definition, in remove]
Ops.remove [definition, in remove]
Ops.remove [definition, in remove]
Ops.remove [definition, in remove]
Ops.remove_min [definition, in remove_min]
Ops.remove_min [definition, in remove_min]
Ops.rev_elements_aux [definition, in rev_elements_aux]
Ops.rev_elements [definition, in rev_elements]
Ops.singleton [definition, in singleton]
Ops.singleton [definition, in singleton]
Ops.singleton [definition, in singleton]
Ops.singleton [definition, in singleton]
Ops.skip_red [definition, in skip_red]
Ops.skip_black [definition, in skip_black]
Ops.split [definition, in split]
Ops.subset [definition, in subset]
Ops.subset [definition, in subset]
Ops.subset [definition, in subset]
Ops.subsetl [definition, in subsetl]
Ops.subsetr [definition, in subsetr]
Ops.t [definition, in t]
Ops.t [definition, in t]
Ops.t [definition, in t]
Ops.t [definition, in t]
Ops.tree [inductive, in tree]
Ops.treeify [definition, in treeify]
Ops.treeify_aux [definition, in treeify_aux]
Ops.treeify_one [definition, in treeify_one]
Ops.treeify_cont [definition, in treeify_cont]
Ops.treeify_zero [definition, in treeify_zero]
Ops.treeify_t [abbreviation, in treeify_t]
Ops.triple [record, in triple]
Ops.t_right [projection, in t_right]
Ops.t_left [projection, in t_left]
Ops.t_in [projection, in t_in]
Ops.union [definition, in union]
Ops.union [definition, in union]
Ops.union [definition, in union]
Ops.union [definition, in union]
Ops.union_list [definition, in union_list]
<< _ , _ , _ >> [notation, in ::'<<'_x_','_x_','_x_'>>']
option [inductive, in option]
option_map [definition, in option_map]
op_rotate [lemma, in op_rotate]
or [inductive, in or]
orb [definition, in orb]
orb_true_iff [lemma, in orb_true_iff]
orb_diag [lemma, in orb_diag]
orb_prop_intro [lemma, in orb_prop_intro]
orb_false_iff [lemma, in orb_false_iff]
orb_andb_distrib_l [lemma, in orb_andb_distrib_l]
orb_prop_elim [lemma, in orb_prop_elim]
orb_false_l [lemma, in orb_false_l]
orb_neg_b [abbreviation, in orb_neg_b]
orb_b_false [abbreviation, in orb_b_false]
orb_true_elim [lemma, in orb_true_elim]
orb_true_l [lemma, in orb_true_l]
orb_b_true [abbreviation, in orb_b_true]
orb_prop2 [abbreviation, in orb_prop2]
orb_false_intro [lemma, in orb_false_intro]
orb_true_b [abbreviation, in orb_true_b]
orb_comm [lemma, in orb_comm]
orb_false_elim [lemma, in orb_false_elim]
orb_andb_distrib_r [lemma, in orb_andb_distrib_r]
orb_negb_r [lemma, in orb_negb_r]
orb_lazy_alt [lemma, in orb_lazy_alt]
orb_false_b [abbreviation, in orb_false_b]
orb_false_r [lemma, in orb_false_r]
orb_assoc [lemma, in orb_assoc]
orb_true_intro [lemma, in orb_true_intro]
orb_prop [lemma, in orb_prop]
orb_true_r [lemma, in orb_true_r]
ord [inductive, in ord]
Order [inductive, in Order]
order [record, in order]
OrderedType [module, in OrderedType]
OrderedType [module, in OrderedType]
OrderedType [library]
OrderedTypeAlt [module, in OrderedTypeAlt]
OrderedTypeAlt [module, in OrderedTypeAlt]
OrderedTypeAlt [library]
OrderedTypeAlt.compare [axiom, in compare]
OrderedTypeAlt.compare [axiom, in compare]
OrderedTypeAlt.compare_trans [axiom, in compare_trans]
OrderedTypeAlt.compare_trans [axiom, in compare_trans]
OrderedTypeAlt.compare_sym [axiom, in compare_sym]
OrderedTypeAlt.compare_sym [axiom, in compare_sym]
OrderedTypeAlt.t [axiom, in t]
OrderedTypeAlt.t [axiom, in t]
_ ?= _ [notation, in ::x_'?='_x]
_ ?= _ [notation, in ::x_'?='_x]
OrderedTypeEx [library]
OrderedTypeFacts [module, in OrderedTypeFacts]
OrderedTypeFacts [module, in OrderedTypeFacts]
OrderedTypeFacts.compare_le_iff [abbreviation, in compare_le_iff]
OrderedTypeFacts.compare_ge_iff [abbreviation, in compare_ge_iff]
OrderedTypeFacts.elim_compare_eq [lemma, in elim_compare_eq]
OrderedTypeFacts.elim_compare_gt [lemma, in elim_compare_gt]
OrderedTypeFacts.elim_compare_lt [lemma, in elim_compare_lt]
OrderedTypeFacts.eqb [definition, in eqb]
OrderedTypeFacts.eqb [definition, in eqb]
OrderedTypeFacts.eqb_alt [lemma, in eqb_alt]
OrderedTypeFacts.eqb_alt [lemma, in eqb_alt]
OrderedTypeFacts.eqb_compat [instance, in eqb_compat]
OrderedTypeFacts.eq_refl [definition, in eq_refl]
OrderedTypeFacts.eq_not_lt [lemma, in eq_not_lt]
OrderedTypeFacts.eq_lt [lemma, in eq_lt]
OrderedTypeFacts.eq_sym [definition, in eq_sym]
OrderedTypeFacts.eq_trans [definition, in eq_trans]
OrderedTypeFacts.eq_dec [definition, in eq_dec]
OrderedTypeFacts.eq_dec [definition, in eq_dec]
OrderedTypeFacts.eq_neq [lemma, in eq_neq]
OrderedTypeFacts.eq_equiv [instance, in eq_equiv]
OrderedTypeFacts.eq_not_gt [lemma, in eq_not_gt]
OrderedTypeFacts.eq_le [lemma, in eq_le]
OrderedTypeFacts.ForNotations [section, in ForNotations]
OrderedTypeFacts.gt_not_eq [lemma, in gt_not_eq]
OrderedTypeFacts.if_eq_dec [lemma, in if_eq_dec]
OrderedTypeFacts.In [abbreviation, in In]
OrderedTypeFacts.Inf [abbreviation, in Inf]
OrderedTypeFacts.Inf_alt [lemma, in Inf_alt]
OrderedTypeFacts.Inf_eq [lemma, in Inf_eq]
OrderedTypeFacts.Inf_lt [lemma, in Inf_lt]
OrderedTypeFacts.In_eq [lemma, in In_eq]
OrderedTypeFacts.In_Inf [lemma, in In_Inf]
OrderedTypeFacts.le_trans [lemma, in le_trans]
OrderedTypeFacts.le_neq [lemma, in le_neq]
OrderedTypeFacts.le_antisym [lemma, in le_antisym]
OrderedTypeFacts.le_lt_trans [lemma, in le_lt_trans]
OrderedTypeFacts.le_eq [lemma, in le_eq]
OrderedTypeFacts.ListIn_Inf [lemma, in ListIn_Inf]
OrderedTypeFacts.ListIn_In [lemma, in ListIn_In]
OrderedTypeFacts.lt_irrefl [definition, in lt_irrefl]
OrderedTypeFacts.lt_compat [instance, in lt_compat]
OrderedTypeFacts.lt_strorder [instance, in lt_strorder]
OrderedTypeFacts.lt_dec [lemma, in lt_dec]
OrderedTypeFacts.lt_dec [lemma, in lt_dec]
OrderedTypeFacts.lt_le_trans [lemma, in lt_le_trans]
OrderedTypeFacts.lt_not_gt [lemma, in lt_not_gt]
OrderedTypeFacts.lt_antirefl [lemma, in lt_antirefl]
OrderedTypeFacts.lt_total [lemma, in lt_total]
OrderedTypeFacts.lt_trans [definition, in lt_trans]
OrderedTypeFacts.lt_eq [lemma, in lt_eq]
OrderedTypeFacts.lt_le [lemma, in lt_le]
OrderedTypeFacts.neq_eq [lemma, in neq_eq]
OrderedTypeFacts.neq_sym [lemma, in neq_sym]
OrderedTypeFacts.NoDup [abbreviation, in NoDup]
OrderedTypeFacts.OrderElts [module, in OrderedTypeFacts.OrderElts]
OrderedTypeFacts.OrderElts.eq [definition, in eq]
OrderedTypeFacts.OrderElts.eq_equiv [definition, in eq_equiv]
OrderedTypeFacts.OrderElts.le [definition, in le]
OrderedTypeFacts.OrderElts.le_lteq [lemma, in le_lteq]
OrderedTypeFacts.OrderElts.lt [definition, in lt]
OrderedTypeFacts.OrderElts.lt_compat [definition, in lt_compat]
OrderedTypeFacts.OrderElts.lt_strorder [definition, in lt_strorder]
OrderedTypeFacts.OrderElts.lt_total [definition, in lt_total]
OrderedTypeFacts.OrderElts.t [definition, in t]
OrderedTypeFacts.OrderTac [module, in OrderedTypeFacts.OrderTac]
OrderedTypeFacts.OrderTac [module, in OrderedTypeFacts.OrderTac]
OrderedTypeFacts.Sort [abbreviation, in Sort]
OrderedTypeFacts.Sort_NoDup [lemma, in Sort_NoDup]
OrderedTypeFacts.Sort_Inf_In [lemma, in Sort_Inf_In]
_ ?= _ (order) [notation, in :order:x_'?='_x]
_ <= _ (order) [notation, in :order:x_'<='_x]
OrderedTypeFull [module, in OrderedTypeFull]
OrderedTypeFullFacts [module, in OrderedTypeFullFacts]
OrderedTypeFullFacts.compare_le_iff [lemma, in compare_le_iff]
OrderedTypeFullFacts.compare_ge_iff [lemma, in compare_ge_iff]
OrderedTypeFullFacts.eq_is_le_ge [lemma, in eq_is_le_ge]
OrderedTypeFullFacts.le_order [instance, in le_order]
OrderedTypeFullFacts.le_compat [instance, in le_compat]
OrderedTypeFullFacts.le_preorder [instance, in le_preorder]
OrderedTypeFullFacts.le_not_gt_iff [lemma, in le_not_gt_iff]
OrderedTypeFullFacts.le_or_gt [lemma, in le_or_gt]
OrderedTypeFullFacts.le_antisym [instance, in le_antisym]
OrderedTypeFullFacts.lt_or_ge [lemma, in lt_or_ge]
OrderedTypeFullFacts.lt_not_ge_iff [lemma, in lt_not_ge_iff]
OrderedTypeFullFacts.OrderTac [module, in OrderedTypeFullFacts.OrderTac]
OrderedTypeFull' [module, in OrderedTypeFull']
OrderedTypeLists [module, in OrderedTypeLists]
OrderedTypeLists.ForNotations [section, in ForNotations]
OrderedTypeLists.In [abbreviation, in In]
OrderedTypeLists.Inf [abbreviation, in Inf]
OrderedTypeLists.Inf_alt [lemma, in Inf_alt]
OrderedTypeLists.Inf_eq [lemma, in Inf_eq]
OrderedTypeLists.Inf_lt [lemma, in Inf_lt]
OrderedTypeLists.In_eq [lemma, in In_eq]
OrderedTypeLists.In_Inf [lemma, in In_Inf]
OrderedTypeLists.ListIn_Inf [lemma, in ListIn_Inf]
OrderedTypeLists.ListIn_In [lemma, in ListIn_In]
OrderedTypeLists.NoDup [abbreviation, in NoDup]
OrderedTypeLists.Sort [abbreviation, in Sort]
OrderedTypeLists.Sort_NoDup [lemma, in Sort_NoDup]
OrderedTypeLists.Sort_Inf_In [lemma, in Sort_Inf_In]
OrderedTypeOrig [module, in OrderedTypeOrig]
OrderedTypeRev [module, in OrderedTypeRev]
OrderedTypeRev.compare [definition, in compare]
OrderedTypeRev.compare_spec [lemma, in compare_spec]
OrderedTypeRev.eq [definition, in eq]
OrderedTypeRev.eq_dec [definition, in eq_dec]
OrderedTypeRev.eq_equiv [instance, in eq_equiv]
OrderedTypeRev.le [definition, in le]
OrderedTypeRev.le_lteq [lemma, in le_lteq]
OrderedTypeRev.lt [definition, in lt]
OrderedTypeRev.lt_compat [instance, in lt_compat]
OrderedTypeRev.lt_strorder [instance, in lt_strorder]
OrderedTypeRev.t [definition, in t]
OrderedTypeTest [module, in OrderedTypeTest]
OrderedTypeTest.eq_not_lt [lemma, in eq_not_lt]
OrderedTypeTest.eq_lt [lemma, in eq_lt]
OrderedTypeTest.eq_is_nlt_ngt [lemma, in eq_is_nlt_ngt]
OrderedTypeTest.eq_neq [lemma, in eq_neq]
OrderedTypeTest.eq_not_gt [lemma, in eq_not_gt]
OrderedTypeTest.eq_le [lemma, in eq_le]
OrderedTypeTest.gt_not_eq [lemma, in gt_not_eq]
OrderedTypeTest.le_trans [lemma, in le_trans]
OrderedTypeTest.le_neq [lemma, in le_neq]
OrderedTypeTest.le_antisym [lemma, in le_antisym]
OrderedTypeTest.le_lt_trans [lemma, in le_lt_trans]
OrderedTypeTest.le_eq [lemma, in le_eq]
OrderedTypeTest.lt_le_trans [lemma, in lt_le_trans]
OrderedTypeTest.lt_not_gt [lemma, in lt_not_gt]
OrderedTypeTest.lt_not_eq [lemma, in lt_not_eq]
OrderedTypeTest.lt_eq [lemma, in lt_eq]
OrderedTypeTest.lt_le [lemma, in lt_le]
OrderedTypeTest.MO [module, in OrderedTypeTest.MO]
OrderedTypeTest.neq_eq [lemma, in neq_eq]
OrderedTypeTest.neq_sym [lemma, in neq_sym]
OrderedTypeWithLeibniz [module, in OrderedTypeWithLeibniz]
OrderedTypeWithLeibniz.eq_leibniz [axiom, in eq_leibniz]
OrderedType_from_Alt.eq_refl [lemma, in eq_refl]
OrderedType_from_Alt [module, in OrderedType_from_Alt]
OrderedType_to_Alt.t [definition, in t]
OrderedType_from_Alt.t [definition, in t]
OrderedType_to_Alt.compare [definition, in compare]
OrderedType_from_Alt.compare [definition, in compare]
OrderedType_to_Alt.compare_trans [lemma, in compare_trans]
OrderedType_to_Alt [module, in OrderedType_to_Alt]
OrderedType_from_Alt.eq_sym [lemma, in eq_sym]
OrderedType_from_Alt.lt_not_eq [lemma, in lt_not_eq]
OrderedType_to_Alt.MO [module, in OrderedType_to_Alt.MO]
OrderedType_from_Alt.lt_trans [definition, in lt_trans]
OrderedType_from_Alt.eq_trans [definition, in eq_trans]
OrderedType_to_Alt.compare_sym [lemma, in compare_sym]
OrderedType_from_Alt.eq_dec [definition, in eq_dec]
OrderedType_from_Alt.lt [definition, in lt]
_ ?= _ [notation, in ::x_'?='_x]
OrderedType_from_Alt.eq [definition, in eq]
OrderedType' [module, in OrderedType']
OrderedType.eq_dec [axiom, in eq_dec]
ordered_Rlist [definition, in ordered_Rlist]
OrderFacts [module, in OrderFacts]
OrderFacts.eq_refl [lemma, in eq_refl]
OrderFacts.eq_lt [definition, in eq_lt]
OrderFacts.eq_sym [lemma, in eq_sym]
OrderFacts.eq_trans [definition, in eq_trans]
OrderFacts.eq_neq [lemma, in eq_neq]
OrderFacts.eq_le [definition, in eq_le]
OrderFacts.interp_ord [definition, in interp_ord]
OrderFacts.le_trans [definition, in le_trans]
OrderFacts.le_neq_lt [lemma, in le_neq_lt]
OrderFacts.le_antisym [lemma, in le_antisym]
OrderFacts.le_lt_trans [definition, in le_lt_trans]
OrderFacts.le_refl [lemma, in le_refl]
OrderFacts.le_eq [definition, in le_eq]
OrderFacts.lt_irrefl [lemma, in lt_irrefl]
OrderFacts.lt_le_trans [definition, in lt_le_trans]
OrderFacts.lt_trans [definition, in lt_trans]
OrderFacts.lt_eq [definition, in lt_eq]
OrderFacts.neq_eq [lemma, in neq_eq]
OrderFacts.neq_sym [lemma, in neq_sym]
OrderFacts.not_ge_lt [lemma, in not_ge_lt]
OrderFacts.not_gt_le [lemma, in not_gt_le]
OrderFacts.not_neq_eq [lemma, in not_neq_eq]
OrderFacts.trans [lemma, in trans]
# [notation, in ::'#']
OrderFunctions [module, in OrderFunctions]
OrderFunctions' [module, in OrderFunctions']
Orders [library]
OrdersAlt [library]
OrdersEx [library]
OrdersFacts [library]
OrdersLists [library]
OrdersTac [library]
OrdProperties [module, in OrdProperties]
OrdProperties [module, in OrdProperties]
OrdProperties [module, in OrdProperties]
OrdProperties.Above [definition, in Above]
OrdProperties.Above [definition, in Above]
OrdProperties.Above [definition, in Above]
OrdProperties.Add [abbreviation, in Add]
OrdProperties.add_fold [lemma, in add_fold]
OrdProperties.add_fold [lemma, in add_fold]
OrdProperties.Below [definition, in Below]
OrdProperties.Below [definition, in Below]
OrdProperties.Below [definition, in Below]
OrdProperties.cardinal [abbreviation, in cardinal]
OrdProperties.choose_equal [lemma, in choose_equal]
OrdProperties.choose_equal [lemma, in choose_equal]
OrdProperties.elements_Add_Above [lemma, in elements_Add_Above]
OrdProperties.elements_Add_Above [lemma, in elements_Add_Above]
OrdProperties.elements_Add_Above [lemma, in elements_Add_Above]
OrdProperties.elements_split [lemma, in elements_split]
OrdProperties.elements_split [lemma, in elements_split]
OrdProperties.elements_split [lemma, in elements_split]
OrdProperties.elements_lt [definition, in elements_lt]
OrdProperties.elements_lt [definition, in elements_lt]
OrdProperties.elements_lt [definition, in elements_lt]
OrdProperties.elements_Add_Below [lemma, in elements_Add_Below]
OrdProperties.elements_Add_Below [lemma, in elements_Add_Below]
OrdProperties.elements_Add_Below [lemma, in elements_Add_Below]
OrdProperties.elements_Add [lemma, in elements_Add]
OrdProperties.elements_Add [lemma, in elements_Add]
OrdProperties.elements_Add [lemma, in elements_Add]
OrdProperties.elements_Equal_eqlistA [lemma, in elements_Equal_eqlistA]
OrdProperties.elements_ge [definition, in elements_ge]
OrdProperties.elements_ge [definition, in elements_ge]
OrdProperties.elements_ge [definition, in elements_ge]
OrdProperties.Elt [section, in Elt]
OrdProperties.Elt.Elements [section, in Elements]
OrdProperties.Elt.elt [variable, in elt]
OrdProperties.Elt.Fold_properties [section, in Fold_properties]
OrdProperties.Elt.Induction_Principles [section, in Induction_Principles]
OrdProperties.Elt.Min_Max_Elt [section, in Min_Max_Elt]
OrdProperties.eqk [abbreviation, in eqk]
OrdProperties.eqke [abbreviation, in eqke]
OrdProperties.Equal [abbreviation, in Equal]
OrdProperties.FoldOpt [section, in FoldOpt]
OrdProperties.FoldOpt [section, in FoldOpt]
OrdProperties.FoldOpt.A [variable, in A]
OrdProperties.FoldOpt.A [variable, in A]
OrdProperties.FoldOpt.Comp [variable, in Comp]
OrdProperties.FoldOpt.Comp [variable, in Comp]
OrdProperties.FoldOpt.eqA [variable, in eqA]
OrdProperties.FoldOpt.eqA [variable, in eqA]
OrdProperties.FoldOpt.f [variable, in f]
OrdProperties.FoldOpt.f [variable, in f]
OrdProperties.FoldOpt.st [variable, in st]
OrdProperties.FoldOpt.st [variable, in st]
OrdProperties.fold_Add_Above [lemma, in fold_Add_Above]
OrdProperties.fold_4 [lemma, in fold_4]
OrdProperties.fold_4 [lemma, in fold_4]
OrdProperties.fold_3 [lemma, in fold_3]
OrdProperties.fold_3 [lemma, in fold_3]
OrdProperties.fold_Equal [lemma, in fold_Equal]
OrdProperties.fold_equal [lemma, in fold_equal]
OrdProperties.fold_equal [lemma, in fold_equal]
OrdProperties.fold_Add_Below [lemma, in fold_Add_Below]
OrdProperties.gtb [definition, in gtb]
OrdProperties.gtb [definition, in gtb]
OrdProperties.gtb [definition, in gtb]
OrdProperties.gtb_1 [lemma, in gtb_1]
OrdProperties.gtb_1 [lemma, in gtb_1]
OrdProperties.gtb_1 [lemma, in gtb_1]
OrdProperties.gtb_compat [instance, in gtb_compat]
OrdProperties.gtb_compat [lemma, in gtb_compat]
OrdProperties.gtb_compat [lemma, in gtb_compat]
OrdProperties.leb [definition, in leb]
OrdProperties.leb [definition, in leb]
OrdProperties.leb [definition, in leb]
OrdProperties.leb_compat [instance, in leb_compat]
OrdProperties.leb_compat [lemma, in leb_compat]
OrdProperties.leb_compat [lemma, in leb_compat]
OrdProperties.leb_1 [lemma, in leb_1]
OrdProperties.leb_1 [lemma, in leb_1]
OrdProperties.leb_1 [lemma, in leb_1]
OrdProperties.ltk [abbreviation, in ltk]
OrdProperties.map_induction_max [lemma, in map_induction_max]
OrdProperties.map_induction_min [lemma, in map_induction_min]
OrdProperties.max_elt_aux [definition, in max_elt_aux]
OrdProperties.max_elt_MapsTo [lemma, in max_elt_MapsTo]
OrdProperties.max_elt_Empty [lemma, in max_elt_Empty]
OrdProperties.max_elt [definition, in max_elt]
OrdProperties.max_elt_Above [lemma, in max_elt_Above]
OrdProperties.ME [module, in OrdProperties.ME]
OrdProperties.ME [module, in OrdProperties.ME]
OrdProperties.ME [module, in OrdProperties.ME]
OrdProperties.min_elt_Empty [lemma, in min_elt_Empty]
OrdProperties.min_elt_MapsTo [lemma, in min_elt_MapsTo]
OrdProperties.min_elt_Below [lemma, in min_elt_Below]
OrdProperties.min_elt [definition, in min_elt]
OrdProperties.ML [module, in OrdProperties.ML]
OrdProperties.O [module, in OrdProperties.O]
OrdProperties.P [module, in OrdProperties.P]
OrdProperties.P [module, in OrdProperties.P]
OrdProperties.P [module, in OrdProperties.P]
OrdProperties.remove_fold_2 [lemma, in remove_fold_2]
OrdProperties.remove_fold_2 [lemma, in remove_fold_2]
OrdProperties.set_induction_max [lemma, in set_induction_max]
OrdProperties.set_induction_max [lemma, in set_induction_max]
OrdProperties.set_induction_min [lemma, in set_induction_min]
OrdProperties.set_induction_min [lemma, in set_induction_min]
OrdProperties.sort_equivlistA_eqlistA [lemma, in sort_equivlistA_eqlistA]
OrdProperties.sort_equivlistA_eqlistA [lemma, in sort_equivlistA_eqlistA]
OrdProperties.sort_equivlistA_eqlistA [lemma, in sort_equivlistA_eqlistA]
ord_trans [projection, in ord_trans]
ord_antisym [projection, in ord_antisym]
ord_refl [projection, in ord_refl]
or_to_imply [lemma, in or_to_imply]
or_cancel_l [lemma, in or_cancel_l]
or_not_r_iff_2 [lemma, in or_not_r_iff_2]
or_cancel_r [lemma, in or_cancel_r]
or_assoc [lemma, in or_assoc]
or_iff_compat_r [lemma, in or_iff_compat_r]
or_comm [lemma, in or_comm]
or_not_l_iff_1 [lemma, in or_not_l_iff_1]
or_not_r_iff_1 [lemma, in or_not_r_iff_1]
or_indd [definition, in or_indd]
or_impl_morphism [instance, in or_impl_morphism]
or_not_and [lemma, in or_not_and]
or_not_l_iff_2 [lemma, in or_not_l_iff_2]
or_elim_redr [definition, in or_elim_redr]
or_iff_compat_l [lemma, in or_iff_compat_l]
or_intror [constructor, in or_intror]
or_introl [constructor, in or_introl]
or_elim_redl [definition, in or_elim_redl]
or_iff_morphism [instance, in or_iff_morphism]
OTF_to_TTLB.t [definition, in t]
OTF_to_TTLB.leb_le [lemma, in leb_le]
OTF_to_OrderTac [module, in OTF_to_OrderTac]
OTF_to_TTLB.leb_trans [lemma, in leb_trans]
OTF_LtIsTotal.lt_total [lemma, in lt_total]
OTF_to_TTLB.leb [definition, in leb]
OTF_to_TotalOrder [module, in OTF_to_TotalOrder]
OTF_to_TTLB [module, in OTF_to_TTLB]
OTF_to_TTLB.leb_total [lemma, in leb_total]
OTF_to_OrderTac.TO [module, in OTF_to_OrderTac.TO]
OTF_LtIsTotal [module, in OTF_LtIsTotal]
other_definitions [section, in other_definitions]
OT_to_Full.le_lteq [lemma, in le_lteq]
OT_from_Alt.lt_compat [instance, in lt_compat]
OT_from_Alt.lt_strorder [instance, in lt_strorder]
OT_from_Alt.eq_lt [lemma, in eq_lt]
OT_to_Alt.t [definition, in t]
OT_from_Alt.t [definition, in t]
OT_to_Full [module, in OT_to_Full]
OT_to_Full.le [definition, in le]
OT_from_Alt.compare_spec [lemma, in compare_spec]
OT_to_Alt.compare [definition, in compare]
OT_from_Alt.compare [definition, in compare]
OT_to_Alt.compare_trans [lemma, in compare_trans]
OT_to_OrderTac [module, in OT_to_OrderTac]
OT_to_Alt.compare_Eq [lemma, in compare_Eq]
OT_to_Alt.compare_Lt [lemma, in compare_Lt]
OT_to_OrderTac.OTF [module, in OT_to_OrderTac.OTF]
OT_to_Alt.compare_sym [lemma, in compare_sym]
OT_from_Alt.eq_dec [definition, in eq_dec]
OT_from_Alt.eq_equiv [instance, in eq_equiv]
OT_to_Alt [module, in OT_to_Alt]
OT_from_Alt.lt_eq [lemma, in lt_eq]
OT_as_DT [module, in OT_as_DT]
OT_as_DT [module, in OT_as_DT]
OT_from_Alt.lt [definition, in lt]
_ ?= _ [notation, in ::x_'?='_x]
OT_from_Alt.eq [definition, in eq]
OT_from_Alt [module, in OT_from_Alt]
OT_to_Alt.compare_Gt [lemma, in compare_Gt]
O_or_S [lemma, in O_or_S]
O_witness [definition, in O_witness]
O_S [lemma, in O_S]



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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 entries)
Axiom 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)