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 _ (13562 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 _ (96 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 _ (210 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 _ (71 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 _ (6947 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 _ (306 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 _ (351 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 _ (182 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 _ (295 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 _ (2870 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 _ (286 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 _ (433 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 _ (1189 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 _ (326 entries)

O

O [constructor, in Coq.Init.Datatypes]
O [module, in Coq.FSets.FMapFacts]
OcamlOps [module, in Coq.FSets.FSetFullAVL]
OcamlOps [module, in Coq.FSets.FSetFullAVL]
OcamlOps.add_cardinal [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.bal_cardinal [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.cardinal2 [definition, in Coq.FSets.FSetFullAVL]
OcamlOps.cardinal_e [definition, in Coq.FSets.FSetFullAVL]
OcamlOps.cardinal_e_2 [definition, in Coq.FSets.FSetFullAVL]
OcamlOps.cons_cardinal_e [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.join_cardinal [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_compare [definition, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_compare_alt [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_compare_aux_Cmp [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_compare_Cmp [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_equal [definition, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_equal_alt [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_equal_1 [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_equal_2 [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_subset_alt [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_subset_12 [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_union_alt [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_union_avl [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_union_bst [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.ocaml_union_in [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.split_cardinal_1 [lemma, in Coq.FSets.FSetFullAVL]
OcamlOps.split_cardinal_2 [lemma, in Coq.FSets.FSetFullAVL]
odd [inductive, in Coq.Arith.Even]
odd_div2 [lemma, in Coq.Arith.Div2]
odd_double [lemma, in Coq.Arith.Div2]
odd_even_lem [lemma, in Coq.Arith.Mult]
odd_even_plus [lemma, in Coq.Arith.Even]
odd_mult [lemma, in Coq.Arith.Even]
odd_mult_inv_l [lemma, in Coq.Arith.Even]
odd_mult_inv_r [lemma, in Coq.Arith.Even]
odd_plus_even_inv_l [lemma, in Coq.Arith.Even]
odd_plus_even_inv_r [lemma, in Coq.Arith.Even]
odd_plus_l [lemma, in Coq.Arith.Even]
odd_plus_odd_inv_l [lemma, in Coq.Arith.Even]
odd_plus_odd_inv_r [lemma, in Coq.Arith.Even]
odd_plus_r [lemma, in Coq.Arith.Even]
odd_plus_split [lemma, in Coq.Arith.Even]
odd_S [constructor, in Coq.Arith.Even]
odd_S2n [lemma, in Coq.Arith.Div2]
Omega [lemma, in Coq.Logic.Hurkens]
OmniscientFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
OmniscientFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice_on [definition, in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_small_drinker [lemma, in Coq.Logic.ChoiceFacts]
On [definition, in Coq.Numbers.Cyclic.Int31.Int31]
one [definition, in Coq.Strings.Ascii]
one_IZR_lt1 [lemma, in Coq.Reals.RIneq]
one_IZR_r_R1 [lemma, in Coq.Reals.RIneq]
open_interval [definition, in Coq.Reals.RiemannInt_SF]
open_set [definition, in Coq.Reals.Rtopology]
open_set_P1 [lemma, in Coq.Reals.Rtopology]
open_set_P2 [lemma, in Coq.Reals.Rtopology]
open_set_P3 [lemma, in Coq.Reals.Rtopology]
open_set_P4 [lemma, in Coq.Reals.Rtopology]
open_set_P5 [lemma, in Coq.Reals.Rtopology]
open_set_P6 [lemma, in Coq.Reals.Rtopology]
Operators_Properties [library]
opp [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
opp_c [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
opp_carry [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
opp_compare [definition, in Coq.Numbers.Natural.BigN.Nbasic]
opp_fct [definition, in Coq.Reals.Ranalysis1]
opp_seq [definition, in Coq.Reals.SeqProp]
option [inductive, in Coq.Init.Datatypes]
option_map [definition, in Coq.Init.Datatypes]
op_rotate [lemma, in Coq.Sets.Permut]
or [inductive, in Coq.Init.Logic]
orb [definition, in Coq.Init.Datatypes]
orb_andb_distrib_l [lemma, in Coq.Bool.Bool]
orb_andb_distrib_r [lemma, in Coq.Bool.Bool]
orb_assoc [lemma, in Coq.Bool.Bool]
orb_b_false [abbreviation, in Coq.Bool.Bool]
orb_b_true [abbreviation, in Coq.Bool.Bool]
orb_comm [lemma, in Coq.Bool.Bool]
orb_false_b [abbreviation, in Coq.Bool.Bool]
orb_false_elim [lemma, in Coq.Bool.Bool]
orb_false_intro [lemma, in Coq.Bool.Bool]
orb_false_l [lemma, in Coq.Bool.Bool]
orb_false_r [lemma, in Coq.Bool.Bool]
orb_lazy_alt [lemma, in Coq.Bool.Bool]
orb_negb_r [lemma, in Coq.Bool.Bool]
orb_neg_b [abbreviation, in Coq.Bool.Bool]
orb_prop [lemma, in Coq.Bool.Bool]
orb_prop2 [abbreviation, in Coq.Bool.Bool]
orb_prop_elim [lemma, in Coq.Bool.Bool]
orb_prop_intro [lemma, in Coq.Bool.Bool]
orb_true_b [abbreviation, in Coq.Bool.Bool]
orb_true_elim [lemma, in Coq.Bool.Bool]
orb_true_intro [lemma, in Coq.Bool.Bool]
orb_true_l [lemma, in Coq.Bool.Bool]
orb_true_r [lemma, in Coq.Bool.Bool]
order [record, in Coq.Relations.Relation_Definitions]
Order [inductive, in Coq.Sets.Relations_1]
OrderedType [module, in Coq.FSets.OrderedType]
OrderedType [library]
OrderedTypeAlt [module, in Coq.FSets.OrderedTypeAlt]
OrderedTypeAlt [library]
OrderedTypeAlt.compare [axiom, in Coq.FSets.OrderedTypeAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.FSets.OrderedTypeAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.FSets.OrderedTypeAlt]
OrderedTypeAlt.t [axiom, in Coq.FSets.OrderedTypeAlt]
OrderedTypeEx [library]
OrderedTypeFacts [module, in Coq.FSets.OrderedType]
OrderedTypeFacts.elim_compare_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.elim_compare_gt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.elim_compare_lt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.eqb [definition, in Coq.FSets.OrderedType]
OrderedTypeFacts.eqb_alt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.eq_dec [definition, in Coq.FSets.OrderedType]
OrderedTypeFacts.eq_le [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.eq_lt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.eq_neq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.eq_not_gt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.eq_not_lt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.ForNotations [section, in Coq.FSets.OrderedType]
OrderedTypeFacts.gt_not_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.hide_lt [definition, in Coq.FSets.OrderedType]
OrderedTypeFacts.In [abbreviation, in Coq.FSets.OrderedType]
OrderedTypeFacts.Inf [abbreviation, in Coq.FSets.OrderedType]
OrderedTypeFacts.Inf_alt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.Inf_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.Inf_lt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.In_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.In_Inf [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.le_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.le_lt_trans [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.le_neq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.ListIn_In [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.ListIn_Inf [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.lt_antirefl [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.lt_dec [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.lt_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.lt_le_trans [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.lt_not_gt [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.neq_eq [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.neq_sym [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.NoDup [abbreviation, in Coq.FSets.OrderedType]
OrderedTypeFacts.Sort [abbreviation, in Coq.FSets.OrderedType]
OrderedTypeFacts.Sort_Inf_In [lemma, in Coq.FSets.OrderedType]
OrderedTypeFacts.Sort_NoDup [lemma, in Coq.FSets.OrderedType]
OrderedType.eq_dec [axiom, in Coq.FSets.OrderedType]
OrderedType_from_Alt [module, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.compare [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.eq [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.eq_dec [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.eq_refl [lemma, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.eq_sym [lemma, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.eq_trans [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.lt [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.lt_not_eq [lemma, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.lt_trans [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_from_Alt.t [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_to_Alt [module, in Coq.FSets.OrderedTypeAlt]
OrderedType_to_Alt.compare [definition, in Coq.FSets.OrderedTypeAlt]
OrderedType_to_Alt.compare_sym [lemma, in Coq.FSets.OrderedTypeAlt]
OrderedType_to_Alt.compare_trans [lemma, in Coq.FSets.OrderedTypeAlt]
OrderedType_to_Alt.t [definition, in Coq.FSets.OrderedTypeAlt]
ordered_Rlist [definition, in Coq.Reals.RList]
OrdProperties [module, in Coq.FSets.FSetProperties]
OrdProperties [module, in Coq.FSets.FMapFacts]
OrdProperties.Above [definition, in Coq.FSets.FMapFacts]
OrdProperties.Above [definition, in Coq.FSets.FSetProperties]
OrdProperties.Add [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.add_fold [lemma, in Coq.FSets.FSetProperties]
OrdProperties.Below [definition, in Coq.FSets.FMapFacts]
OrdProperties.Below [definition, in Coq.FSets.FSetProperties]
OrdProperties.cardinal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.choose_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Above [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Equal_eqlistA [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_ge [definition, in Coq.FSets.FSetProperties]
OrdProperties.elements_ge [definition, in Coq.FSets.FMapFacts]
OrdProperties.elements_lt [definition, in Coq.FSets.FMapFacts]
OrdProperties.elements_lt [definition, in Coq.FSets.FSetProperties]
OrdProperties.elements_split [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_split [lemma, in Coq.FSets.FSetProperties]
OrdProperties.Elt [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Elements [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.elt [variable, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Fold_properties [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Induction_Principles [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Min_Max_Elt [section, in Coq.FSets.FMapFacts]
OrdProperties.eqk [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.eqke [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.Equal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.FoldOpt [section, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.FSets.FSetProperties]
OrdProperties.fold_Add_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_Add_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_Equal [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.fold_3 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.fold_4 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb [definition, in Coq.FSets.FSetProperties]
OrdProperties.gtb [definition, in Coq.FSets.FMapFacts]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FMapFacts]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb_1 [lemma, in Coq.FSets.FMapFacts]
OrdProperties.gtb_1 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb [definition, in Coq.FSets.FSetProperties]
OrdProperties.leb [definition, in Coq.FSets.FMapFacts]
OrdProperties.leb_compat [lemma, in Coq.FSets.FMapFacts]
OrdProperties.leb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb_1 [lemma, in Coq.FSets.FMapFacts]
OrdProperties.leb_1 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.ltk [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.map_induction_max [lemma, in Coq.FSets.FMapFacts]
OrdProperties.map_induction_min [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt [definition, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_aux [definition, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Empty [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_MapsTo [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt [definition, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_Empty [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_MapsTo [lemma, in Coq.FSets.FMapFacts]
OrdProperties.remove_fold_2 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FMapFacts]
ord_antisym [projection, in Coq.Relations.Relation_Definitions]
ord_refl [projection, in Coq.Relations.Relation_Definitions]
ord_trans [projection, in Coq.Relations.Relation_Definitions]
or_cancel_l [lemma, in Coq.Init.Logic]
or_cancel_r [lemma, in Coq.Init.Logic]
or_elim_redl [definition, in Coq.Logic.ClassicalFacts]
or_elim_redr [definition, in Coq.Logic.ClassicalFacts]
or_iff_compat_l [lemma, in Coq.Init.Logic]
or_iff_compat_r [lemma, in Coq.Init.Logic]
or_iff_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_impl_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_introl [constructor, in Coq.Init.Logic]
or_intror [constructor, in Coq.Init.Logic]
or_not_and [lemma, in Coq.Logic.Classical_Prop]
or_not_l_iff_1 [lemma, in Coq.Logic.Decidable]
or_not_l_iff_2 [lemma, in Coq.Logic.Decidable]
or_not_r_iff_1 [lemma, in Coq.Logic.Decidable]
or_not_r_iff_2 [lemma, in Coq.Logic.Decidable]
or_to_imply [lemma, in Coq.Logic.Classical_Prop]
other_definitions [section, in Coq.Lists.ListSet]
other_definitions.A [variable, in Coq.Lists.ListSet]
other_definitions.B [variable, in Coq.Lists.ListSet]
OT_as_DT [module, in Coq.Logic.DecidableTypeEx]
O_or_S [lemma, in Coq.Arith.Peano_dec]
O_S [lemma, in Coq.Init.Peano]



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 _ (13562 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 _ (96 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 _ (210 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 _ (71 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 _ (6947 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 _ (306 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 _ (351 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 _ (182 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 _ (295 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 _ (2870 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 _ (286 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 _ (433 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 _ (1189 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 _ (326 entries)