| 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 | (25786 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 | (996 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 | (807 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 | (1538 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 | (584 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 | (11835 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 | (956 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 | (627 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 | (306 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 | (475 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 | (493 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 | (903 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 | (1194 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 | (4910 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 | (162 entries) |
F
f [projection, in Coq.Reals.Rtopology]f [definition, in Coq.Logic.Berardi]
F [projection, in Coq.Logic.ClassicalFacts]
F [definition, in Coq.micromega.ZMicromega]
fact [definition, in Coq.Arith.Factorial]
Factorial [library]
Facts [section, in Coq.Lists.List]
Facts [module, in Coq.FSets.FMapFacts]
Facts [module, in Coq.MSets.MSetFacts]
Facts [module, in Coq.FSets.FSetFacts]
Facts.A [variable, in Coq.Lists.List]
fact_simpl [lemma, in Coq.Reals.Rfunctions]
fact_le [lemma, in Coq.Arith.Factorial]
fact_neq_0 [lemma, in Coq.Arith.Factorial]
fact_prodSO [lemma, in Coq.Reals.Rprod]
false [constructor, in Coq.Init.Datatypes]
False [inductive, in Coq.Init.Logic]
falseP [constructor, in Coq.Logic.ClassicalFacts]
FalseP [definition, in Coq.Logic.ClassicalFacts]
false_le [lemma, in Coq.Bool.BoolOrder]
false_predicate [definition, in Coq.Classes.RelationClasses]
false_xorb [abbreviation, in Coq.Bool.Bool]
false_hprop [lemma, in Coq.Logic.HLevels]
False_sind [definition, in Coq.Init.Logic]
False_rec [definition, in Coq.Init.Logic]
False_ind [definition, in Coq.Init.Logic]
False_rect [definition, in Coq.Init.Logic]
family [record, in Coq.Reals.Rtopology]
family_closed_set [definition, in Coq.Reals.Rtopology]
family_P1 [lemma, in Coq.Reals.Rtopology]
family_finite [definition, in Coq.Reals.Rtopology]
family_open_set [definition, in Coq.Reals.Rtopology]
Fapp [definition, in Coq.setoid_ring.Field_theory]
fast_Zred_factor6 [definition, in Coq.omega.OmegaLemmas]
fast_Zred_factor5 [definition, in Coq.omega.OmegaLemmas]
fast_Zred_factor4 [definition, in Coq.omega.OmegaLemmas]
fast_Zred_factor3 [definition, in Coq.omega.OmegaLemmas]
fast_Zred_factor2 [definition, in Coq.omega.OmegaLemmas]
fast_Zred_factor1 [definition, in Coq.omega.OmegaLemmas]
fast_Zmult_assoc_reverse [definition, in Coq.omega.OmegaLemmas]
fast_Zmult_plus_distr_l [definition, in Coq.omega.OmegaLemmas]
fast_Zopp_mult_distr_r [definition, in Coq.omega.OmegaLemmas]
fast_Zopp_plus_distr [definition, in Coq.omega.OmegaLemmas]
fast_Zmult_comm [definition, in Coq.omega.OmegaLemmas]
fast_Zopp_eq_mult_neg_1 [definition, in Coq.omega.OmegaLemmas]
fast_Zred_factor0 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA14 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA13 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA16 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA15 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA12 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA11 [definition, in Coq.omega.OmegaLemmas]
fast_OMEGA10 [definition, in Coq.omega.OmegaLemmas]
fast_Zplus_permute [definition, in Coq.omega.OmegaLemmas]
fast_Zplus_assoc [definition, in Coq.omega.OmegaLemmas]
fast_Zplus_assoc_reverse [definition, in Coq.omega.OmegaLemmas]
fast_Zplus_comm [definition, in Coq.omega.OmegaLemmas]
Fcons [definition, in Coq.setoid_ring.Field_theory]
fcons_ok [lemma, in Coq.setoid_ring.Field_theory]
Fcons0 [definition, in Coq.setoid_ring.Field_theory]
Fcons00 [definition, in Coq.setoid_ring.Field_theory]
Fcons1 [definition, in Coq.setoid_ring.Field_theory]
Fcons2 [definition, in Coq.setoid_ring.Field_theory]
fct_cte [definition, in Coq.Reals.Ranalysis1]
Fdiv_def [projection, in Coq.setoid_ring.Field_theory]
fe [projection, in Coq.Reals.RiemannInt_SF]
FEadd [constructor, in Coq.setoid_ring.Field_theory]
FEc [constructor, in Coq.setoid_ring.Field_theory]
FEdiv [constructor, in Coq.setoid_ring.Field_theory]
FEeval [definition, in Coq.setoid_ring.Field_theory]
FEI [constructor, in Coq.setoid_ring.Field_theory]
FEinv [constructor, in Coq.setoid_ring.Field_theory]
FEmul [constructor, in Coq.setoid_ring.Field_theory]
FEO [constructor, in Coq.setoid_ring.Field_theory]
FEopp [constructor, in Coq.setoid_ring.Field_theory]
FEpow [constructor, in Coq.setoid_ring.Field_theory]
FEq [constructor, in Coq.Floats.PrimFloat]
FEsub [constructor, in Coq.setoid_ring.Field_theory]
FEX [constructor, in Coq.setoid_ring.Field_theory]
fexp [definition, in Coq.Floats.SpecFloat]
FExpr [inductive, in Coq.setoid_ring.Field_theory]
FExpr_sind [definition, in Coq.setoid_ring.Field_theory]
FExpr_rec [definition, in Coq.setoid_ring.Field_theory]
FExpr_ind [definition, in Coq.setoid_ring.Field_theory]
FExpr_rect [definition, in Coq.setoid_ring.Field_theory]
FF [definition, in Coq.Reals.RList]
FF [constructor, in Coq.micromega.Tauto]
FGt [constructor, in Coq.Floats.PrimFloat]
fg_id' [definition, in Coq.Logic.Adjointification]
fibonacci [definition, in Coq.ZArith.Zgcd_alt]
fibonacci_incr [lemma, in Coq.ZArith.Zgcd_alt]
fibonacci_pos [lemma, in Coq.ZArith.Zgcd_alt]
Field [library]
field_theory [record, in Coq.setoid_ring.Field_theory]
Field_simplify_eq_in_correct [lemma, in Coq.setoid_ring.Field_theory]
Field_simplify_eq_pow_in_correct [lemma, in Coq.setoid_ring.Field_theory]
Field_simplify_aux_ok [lemma, in Coq.setoid_ring.Field_theory]
Field_simplify_eq_pow_correct [lemma, in Coq.setoid_ring.Field_theory]
Field_simplify_eq_correct [lemma, in Coq.setoid_ring.Field_theory]
Field_correct [lemma, in Coq.setoid_ring.Field_theory]
Field_rw_pow_correct [lemma, in Coq.setoid_ring.Field_theory]
Field_rw_correct [lemma, in Coq.setoid_ring.Field_theory]
field_is_integral_domain [lemma, in Coq.setoid_ring.Field_theory]
Field_theory [library]
Field_tac [library]
filter [definition, in Coq.Lists.List]
Filtering [section, in Coq.Lists.List]
Filtering.A [variable, in Coq.Lists.List]
Filtering.eq_dec [variable, in Coq.Lists.List]
filter_length_forallb [lemma, in Coq.Lists.List]
filter_length_le [lemma, in Coq.Lists.List]
filter_length [lemma, in Coq.Lists.List]
filter_ext [lemma, in Coq.Lists.List]
filter_map [lemma, in Coq.Lists.List]
filter_ext_in_iff [lemma, in Coq.Lists.List]
filter_ext_in [lemma, in Coq.Lists.List]
filter_app [lemma, in Coq.Lists.List]
filter_In [lemma, in Coq.Lists.List]
filter_split [lemma, in Coq.Lists.SetoidList]
filter_InA [lemma, in Coq.Lists.SetoidList]
filter_sort [lemma, in Coq.Lists.SetoidList]
Fin [library]
find [definition, in Coq.Lists.List]
find [definition, in Coq.micromega.VarMap]
Find [section, in Coq.Lists.SetoidList]
findA [definition, in Coq.Lists.SetoidList]
findA_NoDupA [lemma, in Coq.Lists.SetoidList]
findex [definition, in Coq.Strings.String]
find_none [lemma, in Coq.Lists.List]
find_some [lemma, in Coq.Lists.List]
find_left_path [lemma, in Coq.Logic.WKL]
Find.A [variable, in Coq.Lists.SetoidList]
Find.B [variable, in Coq.Lists.SetoidList]
Find.eqA [variable, in Coq.Lists.SetoidList]
Find.eqA_dec [variable, in Coq.Lists.SetoidList]
Find.eqA_equiv [variable, in Coq.Lists.SetoidList]
FinFun [library]
Finite [inductive, in Coq.Sets.Finite_sets]
Finite [definition, in Coq.Logic.FinFun]
Finite_downward_closed [lemma, in Coq.Sets.Finite_sets_facts]
finite_cardinal [lemma, in Coq.Sets.Finite_sets_facts]
Finite_sets_facts.U [variable, in Coq.Sets.Finite_sets_facts]
Finite_sets_facts [section, in Coq.Sets.Finite_sets_facts]
Finite_sind [definition, in Coq.Sets.Finite_sets]
Finite_ind [definition, in Coq.Sets.Finite_sets]
finite_greater [lemma, in Coq.Reals.Rseries]
Finite_subset_has_lub [lemma, in Coq.Sets.Integers]
finite_image [lemma, in Coq.Sets.Image]
Finite_Empty_or_not [lemma, in Coq.Logic.FinFun]
Finite_alt [abbreviation, in Coq.Logic.FinFun]
Finite_alt_deprecated [lemma, in Coq.Logic.FinFun]
Finite_dec [lemma, in Coq.Logic.FinFun]
Finite_sets [library]
Finite_sets_facts [library]
Finite' [definition, in Coq.Logic.FinFun]
Finv_l [projection, in Coq.setoid_ring.Field_theory]
Fin_Finite [lemma, in Coq.Logic.FinFun]
Fin2Restrict [module, in Coq.Logic.FinFun]
Fin2Restrict.extend [definition, in Coq.Logic.FinFun]
Fin2Restrict.extend_injective [lemma, in Coq.Logic.FinFun]
Fin2Restrict.extend_surjective [lemma, in Coq.Logic.FinFun]
Fin2Restrict.extend_n2f [lemma, in Coq.Logic.FinFun]
Fin2Restrict.extend_f2n [lemma, in Coq.Logic.FinFun]
Fin2Restrict.extend_ok [lemma, in Coq.Logic.FinFun]
Fin2Restrict.f2n [definition, in Coq.Logic.FinFun]
Fin2Restrict.f2n_inj [definition, in Coq.Logic.FinFun]
Fin2Restrict.f2n_n2f [definition, in Coq.Logic.FinFun]
Fin2Restrict.f2n_ok [definition, in Coq.Logic.FinFun]
Fin2Restrict.n2f [abbreviation, in Coq.Logic.FinFun]
Fin2Restrict.n2f_ext [definition, in Coq.Logic.FinFun]
Fin2Restrict.n2f_f2n [definition, in Coq.Logic.FinFun]
Fin2Restrict.restrict [definition, in Coq.Logic.FinFun]
Fin2Restrict.restrict_injective [lemma, in Coq.Logic.FinFun]
Fin2Restrict.restrict_surjective [lemma, in Coq.Logic.FinFun]
Fin2Restrict.restrict_n2f [lemma, in Coq.Logic.FinFun]
Fin2Restrict.restrict_f2n [lemma, in Coq.Logic.FinFun]
firstn [definition, in Coq.Lists.List]
firstn_map [lemma, in Coq.Lists.List]
firstn_removelast [lemma, in Coq.Lists.List]
firstn_rev [lemma, in Coq.Lists.List]
firstn_skipn_rev [lemma, in Coq.Lists.List]
firstn_length [lemma, in Coq.Lists.List]
firstn_skipn [lemma, in Coq.Lists.List]
firstn_skipn_comm [lemma, in Coq.Lists.List]
firstn_firstn [lemma, in Coq.Lists.List]
firstn_app_2 [lemma, in Coq.Lists.List]
firstn_app [lemma, in Coq.Lists.List]
firstn_length_le [lemma, in Coq.Lists.List]
firstn_le_length [lemma, in Coq.Lists.List]
firstn_O [lemma, in Coq.Lists.List]
firstn_all2 [lemma, in Coq.Lists.List]
firstn_all [lemma, in Coq.Lists.List]
firstn_cons [lemma, in Coq.Lists.List]
firstn_nil [lemma, in Coq.Lists.List]
first_indices_increasing [lemma, in Coq.Reals.Runcountable]
first_two_in_interval_works [lemma, in Coq.Reals.Runcountable]
first_two_in_interval [definition, in Coq.Reals.Runcountable]
first_in_holed_interval_works [lemma, in Coq.Reals.Runcountable]
first_in_holed_interval [definition, in Coq.Reals.Runcountable]
first_definitions.Aeq_dec [variable, in Coq.Lists.ListSet]
first_definitions.A [variable, in Coq.Lists.ListSet]
first_definitions [section, in Coq.Lists.ListSet]
Fix [definition, in Coq.Init.Wf]
Fix [projection, in Coq.Logic.ClassicalFacts]
Fix_sub_rect [lemma, in Coq.Program.Wf]
Fix_rects.equiv_lowers [variable, in Coq.Program.Wf]
Fix_F_sub_rect [lemma, in Coq.Program.Wf]
Fix_rects.f [variable, in Coq.Program.Wf]
Fix_rects.Rwf [variable, in Coq.Program.Wf]
Fix_rects.R [variable, in Coq.Program.Wf]
Fix_rects.P [variable, in Coq.Program.Wf]
Fix_rects.A [variable, in Coq.Program.Wf]
Fix_rects [section, in Coq.Program.Wf]
fix_sub_eq [lemma, in Coq.Program.Wf]
Fix_eq [lemma, in Coq.Program.Wf]
Fix_F_inv [lemma, in Coq.Program.Wf]
Fix_F_eq [lemma, in Coq.Program.Wf]
Fix_sub [definition, in Coq.Program.Wf]
Fix_F_sub [definition, in Coq.Program.Wf]
Fix_F_2 [definition, in Coq.Init.Wf]
Fix_eq [lemma, in Coq.Init.Wf]
Fix_F_inv [lemma, in Coq.Init.Wf]
Fix_F_eq [lemma, in Coq.Init.Wf]
Fix_F [definition, in Coq.Init.Wf]
fix_proto [definition, in Coq.Program.Tactics]
FlatMap [section, in Coq.Lists.List]
FlatMap.A [variable, in Coq.Lists.List]
FlatMap.B [variable, in Coq.Lists.List]
FlatMap.f [variable, in Coq.Lists.List]
flatten_cmp_opt [definition, in Coq.Floats.FloatAxioms]
flat_map_constant_length [lemma, in Coq.Lists.List]
flat_map_length [lemma, in Coq.Lists.List]
flat_map_ext [lemma, in Coq.Lists.List]
flat_map_app [lemma, in Coq.Lists.List]
flat_map_concat_map [lemma, in Coq.Lists.List]
flat_map [definition, in Coq.Lists.List]
flat_spec_sind [definition, in Coq.Sorting.Heap]
flat_spec_rec [definition, in Coq.Sorting.Heap]
flat_spec_ind [definition, in Coq.Sorting.Heap]
flat_spec_rect [definition, in Coq.Sorting.Heap]
flat_exist [constructor, in Coq.Sorting.Heap]
flat_spec [inductive, in Coq.Sorting.Heap]
Flhs [projection, in Coq.micromega.RingMicromega]
flip [definition, in Coq.Classes.CRelationClasses]
flip [definition, in Coq.Program.Basics]
flip_Equivalence [lemma, in Coq.Classes.RelationClasses]
flip_PER [lemma, in Coq.Classes.RelationClasses]
flip_StrictOrder [lemma, in Coq.Classes.RelationClasses]
flip_PreOrder [lemma, in Coq.Classes.RelationClasses]
flip_Antisymmetric [definition, in Coq.Classes.RelationClasses]
flip_Transitive [definition, in Coq.Classes.RelationClasses]
flip_Asymmetric [definition, in Coq.Classes.RelationClasses]
flip_Symmetric [definition, in Coq.Classes.RelationClasses]
flip_Irreflexive [definition, in Coq.Classes.RelationClasses]
flip_Reflexive [lemma, in Coq.Classes.RelationClasses]
flip_arrow [lemma, in Coq.Classes.Morphisms]
flip_atom [lemma, in Coq.Classes.Morphisms]
flip_pars [instance, in Coq.Classes.Morphisms]
flip_respectful [lemma, in Coq.Classes.Morphisms]
flip_proper [definition, in Coq.Classes.Morphisms]
flip_arrow [lemma, in Coq.Classes.CMorphisms]
flip_atom [lemma, in Coq.Classes.CMorphisms]
flip_respectful [lemma, in Coq.Classes.CMorphisms]
flip_proper [definition, in Coq.Classes.CMorphisms]
flip_Equivalence [lemma, in Coq.Classes.CRelationClasses]
flip_PER [lemma, in Coq.Classes.CRelationClasses]
flip_StrictOrder [lemma, in Coq.Classes.CRelationClasses]
flip_PreOrder [lemma, in Coq.Classes.CRelationClasses]
flip_Antisymmetric [definition, in Coq.Classes.CRelationClasses]
flip_Transitive [definition, in Coq.Classes.CRelationClasses]
flip_Asymmetric [definition, in Coq.Classes.CRelationClasses]
flip_Symmetric [definition, in Coq.Classes.CRelationClasses]
flip_Irreflexive [definition, in Coq.Classes.CRelationClasses]
flip_Reflexive [lemma, in Coq.Classes.CRelationClasses]
flip_flip [lemma, in Coq.Program.Combinators]
flip_pointwise_relation [lemma, in Coq.Classes.Morphisms_Relations]
flip1 [lemma, in Coq.Classes.Morphisms]
flip1 [lemma, in Coq.Classes.CMorphisms]
flip2 [lemma, in Coq.Classes.Morphisms]
flip2 [lemma, in Coq.Classes.CMorphisms]
float [axiom, in Coq.Floats.PrimFloat]
Float [library]
FloatAxioms [library]
FloatClass [library]
FloatLemmas [library]
FloatOps [section, in Coq.Floats.SpecFloat]
FloatOps [library]
FloatOps.emax [variable, in Coq.Floats.SpecFloat]
FloatOps.Iter [section, in Coq.Floats.SpecFloat]
FloatOps.Iter.f [variable, in Coq.Floats.SpecFloat]
FloatOps.prec [variable, in Coq.Floats.SpecFloat]
FloatOps.Rounding [section, in Coq.Floats.SpecFloat]
FloatOps.ValidBinary [section, in Coq.Floats.SpecFloat]
FloatOps.Zdigits2 [section, in Coq.Floats.SpecFloat]
Floats [library]
float_wrap [projection, in Coq.Floats.PrimFloat]
float_wrapper [record, in Coq.Floats.PrimFloat]
float_comparison [inductive, in Coq.Floats.PrimFloat]
float_class [inductive, in Coq.Floats.FloatClass]
floor [definition, in Coq.ZArith.Zcomplements]
floor_ok [lemma, in Coq.ZArith.Zcomplements]
floor_gt0 [lemma, in Coq.ZArith.Zcomplements]
floor_pos [definition, in Coq.ZArith.Zcomplements]
FLt [constructor, in Coq.Floats.PrimFloat]
FMap [library]
FMapAVL [library]
FMapFacts [library]
FMapFullAVL [library]
FMapInterface [library]
FMapList [library]
FMapPositive [library]
FMaps [library]
FMapWeakList [library]
Fnorm [definition, in Coq.setoid_ring.Field_theory]
Fnorm_ok [lemma, in Coq.setoid_ring.Field_theory]
Fnorm_crossproduct [lemma, in Coq.setoid_ring.Field_theory]
Fnorm_FEeval_PEeval [lemma, in Coq.setoid_ring.Field_theory]
FNotComparable [constructor, in Coq.Floats.PrimFloat]
foldA [definition, in Coq.micromega.Tauto]
fold_left_rev_right [lemma, in Coq.Vectors.VectorSpec]
fold_right_shiftin [lemma, in Coq.Vectors.VectorSpec]
fold_left_right_assoc_eq [lemma, in Coq.Vectors.VectorSpec]
fold_symmetric [lemma, in Coq.Lists.List]
fold_left_rev_right [lemma, in Coq.Lists.List]
fold_right_app [lemma, in Coq.Lists.List]
fold_right [definition, in Coq.Lists.List]
Fold_Right_Recursor.a0 [variable, in Coq.Lists.List]
Fold_Right_Recursor.f [variable, in Coq.Lists.List]
Fold_Right_Recursor.B [variable, in Coq.Lists.List]
Fold_Right_Recursor.A [variable, in Coq.Lists.List]
Fold_Right_Recursor [section, in Coq.Lists.List]
fold_left_length [lemma, in Coq.Lists.List]
fold_left_app [lemma, in Coq.Lists.List]
fold_left [definition, in Coq.Lists.List]
Fold_Left_Recursor.f [variable, in Coq.Lists.List]
Fold_Left_Recursor.B [variable, in Coq.Lists.List]
Fold_Left_Recursor.A [variable, in Coq.Lists.List]
Fold_Left_Recursor [section, in Coq.Lists.List]
fold_left2 [definition, in Coq.Vectors.VectorDef]
fold_right2 [definition, in Coq.Vectors.VectorDef]
fold_right [definition, in Coq.Vectors.VectorDef]
fold_left [definition, in Coq.Vectors.VectorDef]
fold_right_add2 [lemma, in Coq.Lists.SetoidList]
fold_right_equivlistA2 [lemma, in Coq.Lists.SetoidList]
fold_right_commutes2 [lemma, in Coq.Lists.SetoidList]
fold_right_add_restr2 [lemma, in Coq.Lists.SetoidList]
fold_right_equivlistA_restr2 [lemma, in Coq.Lists.SetoidList]
fold_right_commutes_restr2 [lemma, in Coq.Lists.SetoidList]
fold_right_eqlistA2 [lemma, in Coq.Lists.SetoidList]
fold_right_add [lemma, in Coq.Lists.SetoidList]
fold_right_equivlistA [lemma, in Coq.Lists.SetoidList]
fold_right_commutes [lemma, in Coq.Lists.SetoidList]
fold_right_add_restr [lemma, in Coq.Lists.SetoidList]
fold_right_equivlistA_restr [lemma, in Coq.Lists.SetoidList]
fold_right_commutes_restr [lemma, in Coq.Lists.SetoidList]
fold_right_eqlistA [lemma, in Coq.Lists.SetoidList]
Fop [projection, in Coq.micromega.RingMicromega]
FOP_cons [constructor, in Coq.Lists.List]
FOP_nil [constructor, in Coq.Lists.List]
ForAll [inductive, in Coq.Lists.Streams]
Forall [inductive, in Coq.Lists.List]
Forall [inductive, in Coq.Vectors.VectorDef]
forallb [definition, in Coq.Lists.List]
forallb_filter_id [lemma, in Coq.Lists.List]
forallb_filter [lemma, in Coq.Lists.List]
forallb_app [lemma, in Coq.Lists.List]
forallb_forall [lemma, in Coq.Lists.List]
ForallOrdPairs [inductive, in Coq.Lists.List]
ForallOrdPairs_ForallPairs [lemma, in Coq.Lists.List]
ForallOrdPairs_In [lemma, in Coq.Lists.List]
ForallOrdPairs_sind [definition, in Coq.Lists.List]
ForallOrdPairs_ind [definition, in Coq.Lists.List]
ForallOrdPairs_inclA [lemma, in Coq.Lists.SetoidList]
ForallPairs [definition, in Coq.Lists.List]
ForallPairs [section, in Coq.Lists.List]
ForallPairs_ForallOrdPairs [lemma, in Coq.Lists.List]
ForallPairs.A [variable, in Coq.Lists.List]
ForallPairs.R [variable, in Coq.Lists.List]
ForAll_map [lemma, in Coq.Lists.Streams]
ForAll_coind [lemma, in Coq.Lists.Streams]
ForAll_Str_nth_tl [lemma, in Coq.Lists.Streams]
Forall_rev [lemma, in Coq.Vectors.VectorSpec]
Forall_shiftin [lemma, in Coq.Vectors.VectorSpec]
Forall_nth_order [lemma, in Coq.Vectors.VectorSpec]
Forall_nth [lemma, in Coq.Vectors.VectorSpec]
Forall_append [lemma, in Coq.Vectors.VectorSpec]
Forall_map [lemma, in Coq.Vectors.VectorSpec]
Forall_cons_iff [lemma, in Coq.Vectors.VectorSpec]
Forall_forall [lemma, in Coq.Vectors.VectorSpec]
Forall_impl [lemma, in Coq.Vectors.VectorSpec]
Forall_eq_repeat [lemma, in Coq.Lists.List]
Forall_Exists_exists_Forall2 [lemma, in Coq.Lists.List]
Forall_image [lemma, in Coq.Lists.List]
Forall_flat_map [lemma, in Coq.Lists.List]
Forall_concat [lemma, in Coq.Lists.List]
Forall_map [lemma, in Coq.Lists.List]
Forall_Exists_dec [lemma, in Coq.Lists.List]
Forall_Exists_neg [lemma, in Coq.Lists.List]
Forall_and_inv [lemma, in Coq.Lists.List]
Forall_and [lemma, in Coq.Lists.List]
Forall_impl [lemma, in Coq.Lists.List]
Forall_fold_right [lemma, in Coq.Lists.List]
Forall_dec [lemma, in Coq.Lists.List]
Forall_rect [lemma, in Coq.Lists.List]
Forall_rev [lemma, in Coq.Lists.List]
Forall_elt [lemma, in Coq.Lists.List]
Forall_app [lemma, in Coq.Lists.List]
Forall_nth [lemma, in Coq.Lists.List]
Forall_forall [lemma, in Coq.Lists.List]
Forall_cons_iff [lemma, in Coq.Lists.List]
Forall_nil_iff [lemma, in Coq.Lists.List]
Forall_inv_tail [lemma, in Coq.Lists.List]
Forall_inv [lemma, in Coq.Lists.List]
Forall_sind [definition, in Coq.Lists.List]
Forall_ind [definition, in Coq.Lists.List]
Forall_cons [constructor, in Coq.Lists.List]
Forall_nil [constructor, in Coq.Lists.List]
forall_subrelation [lemma, in Coq.Classes.Morphisms]
forall_relation [definition, in Coq.Classes.Morphisms]
forall_def [definition, in Coq.Classes.Morphisms]
forall_eq_rect_comp [definition, in Coq.Logic.FunctionalExtensionality]
forall_eq_rect [definition, in Coq.Logic.FunctionalExtensionality]
forall_sig_eq_rect [lemma, in Coq.Logic.FunctionalExtensionality]
forall_extensionalityS [lemma, in Coq.Logic.FunctionalExtensionality]
forall_extensionalityP [lemma, in Coq.Logic.FunctionalExtensionality]
forall_extensionality [lemma, in Coq.Logic.FunctionalExtensionality]
forall_subrelation [lemma, in Coq.Classes.CMorphisms]
forall_relation [definition, in Coq.Classes.CMorphisms]
forall_def [definition, in Coq.Classes.CMorphisms]
forall_hprop [lemma, in Coq.Logic.HLevels]
forall_exists_coincide_unique_domain [lemma, in Coq.Init.Logic]
forall_exists_unique_domain_coincide [lemma, in Coq.Init.Logic]
Forall_sind [definition, in Coq.Vectors.VectorDef]
Forall_ind [definition, in Coq.Vectors.VectorDef]
Forall_cons [constructor, in Coq.Vectors.VectorDef]
Forall_nil [constructor, in Coq.Vectors.VectorDef]
Forall2 [inductive, in Coq.Lists.List]
Forall2 [section, in Coq.Lists.List]
Forall2 [inductive, in Coq.Vectors.VectorDef]
Forall2_append [lemma, in Coq.Vectors.VectorSpec]
Forall2_nth_order [lemma, in Coq.Vectors.VectorSpec]
Forall2_nth [lemma, in Coq.Vectors.VectorSpec]
Forall2_flip [lemma, in Coq.Lists.List]
Forall2_impl [lemma, in Coq.Lists.List]
Forall2_app [lemma, in Coq.Lists.List]
Forall2_app_inv_r [lemma, in Coq.Lists.List]
Forall2_app_inv_l [lemma, in Coq.Lists.List]
Forall2_length [lemma, in Coq.Lists.List]
Forall2_cons_iff [lemma, in Coq.Lists.List]
Forall2_refl [lemma, in Coq.Lists.List]
Forall2_sind [definition, in Coq.Lists.List]
Forall2_ind [definition, in Coq.Lists.List]
Forall2_cons [constructor, in Coq.Lists.List]
Forall2_nil [constructor, in Coq.Lists.List]
Forall2_sind [definition, in Coq.Vectors.VectorDef]
Forall2_ind [definition, in Coq.Vectors.VectorDef]
Forall2_cons [constructor, in Coq.Vectors.VectorDef]
Forall2_nil [constructor, in Coq.Vectors.VectorDef]
Forall2.A [variable, in Coq.Lists.List]
Forall2.B [variable, in Coq.Lists.List]
Forall2.R [variable, in Coq.Lists.List]
forE [lemma, in Coq.ssr.ssrbool]
form [inductive, in Coq.rtauto.Rtauto]
Format [module, in Ltac2.Message]
Formula [record, in Coq.micromega.RingMicromega]
formula [inductive, in Coq.btauto.Reflect]
formula_eval [definition, in Coq.btauto.Reflect]
formula_sind [definition, in Coq.btauto.Reflect]
formula_rec [definition, in Coq.btauto.Reflect]
formula_ind [definition, in Coq.btauto.Reflect]
formula_rect [definition, in Coq.btauto.Reflect]
formula_ifb [constructor, in Coq.btauto.Reflect]
formula_xor [constructor, in Coq.btauto.Reflect]
formula_neg [constructor, in Coq.btauto.Reflect]
formula_dsj [constructor, in Coq.btauto.Reflect]
formula_cnj [constructor, in Coq.btauto.Reflect]
formula_top [constructor, in Coq.btauto.Reflect]
formula_btm [constructor, in Coq.btauto.Reflect]
formula_var [constructor, in Coq.btauto.Reflect]
formule [lemma, in Coq.Reals.Ranalysis2]
form_eq_refl [lemma, in Coq.rtauto.Rtauto]
form_eq [definition, in Coq.rtauto.Rtauto]
form_sind [definition, in Coq.rtauto.Rtauto]
form_rec [definition, in Coq.rtauto.Rtauto]
form_ind [definition, in Coq.rtauto.Rtauto]
form_rect [definition, in Coq.rtauto.Rtauto]
form1 [lemma, in Coq.Reals.Rtrigo1]
form2 [lemma, in Coq.Reals.Rtrigo1]
form3 [lemma, in Coq.Reals.Rtrigo1]
form4 [lemma, in Coq.Reals.Rtrigo1]
for_base_fp [lemma, in Coq.Reals.R_Ifp]
Fourier [library]
Fourier_util [library]
fp_nat [lemma, in Coq.Reals.R_Ifp]
fp_R0 [lemma, in Coq.Reals.R_Ifp]
frac_part [definition, in Coq.Reals.R_Ifp]
frame_tan [definition, in Coq.Reals.Ratan]
Free [module, in Ltac2.Fresh]
frefl [lemma, in Coq.ssr.ssrfun]
Fresh [library]
Frhs [projection, in Coq.micromega.RingMicromega]
frshiftexp [axiom, in Coq.Floats.PrimFloat]
frshiftexp_spec [axiom, in Coq.Floats.FloatAxioms]
FS [constructor, in Coq.Vectors.Fin]
FSet [library]
FSetAVL [library]
FSetBridge [library]
FSetCompat [library]
FSetDecide [library]
FSetEqProperties [library]
FSetFacts [library]
FSetInterface [library]
FSetList [library]
FSetPositive [library]
FSetProperties [library]
FSets [library]
FSetToFiniteSet [library]
FSetWeakList [library]
Fst [abbreviation, in Coq.Classes.RelationPairs]
fst [definition, in Coq.Init.Datatypes]
FstRel_sub [instance, in Coq.Classes.RelationPairs]
FstRel_ProdRel [lemma, in Coq.Classes.RelationPairs]
fstT [abbreviation, in Coq.Init.Datatypes]
fst_compat [instance, in Coq.Classes.RelationPairs]
fst_measure [instance, in Coq.Classes.RelationPairs]
fsym [lemma, in Coq.ssr.ssrfun]
FS_inj [definition, in Coq.Vectors.Fin]
FTCN_step1 [lemma, in Coq.Reals.NewtonInt]
FTC_Riemann [lemma, in Coq.Reals.RiemannInt]
FTC_P1 [lemma, in Coq.Reals.RiemannInt]
FTC_Newton [lemma, in Coq.Reals.NewtonInt]
ftrans [lemma, in Coq.ssr.ssrfun]
Full [inductive, in Coq.rtauto.Bintree]
Full [definition, in Coq.Logic.FinFun]
Fullset [definition, in Coq.Sets.Uniset]
Full_set_sind [definition, in Coq.Sets.Ensembles]
Full_set_ind [definition, in Coq.Sets.Ensembles]
Full_intro [constructor, in Coq.Sets.Ensembles]
Full_set [inductive, in Coq.Sets.Ensembles]
Full_map [lemma, in Coq.rtauto.Bintree]
Full_index_one_empty [lemma, in Coq.rtauto.Bintree]
Full_push_compat [lemma, in Coq.rtauto.Bintree]
Full_sind [definition, in Coq.rtauto.Bintree]
Full_rec [definition, in Coq.rtauto.Bintree]
Full_ind [definition, in Coq.rtauto.Bintree]
Full_rect [definition, in Coq.rtauto.Bintree]
FunChoice_Equiv_RelChoice_and_ParamDefinDescr [abbreviation, in Coq.Logic.ChoiceFacts]
FunctExt_BijComp [lemma, in Coq.Logic.ExtensionalityFacts]
FunctExt_iff_UniqInverse [lemma, in Coq.Logic.ExtensionalityFacts]
FunctExt_UniqInverse [lemma, in Coq.Logic.ExtensionalityFacts]
FunctExt_iff_EqDeltaProjs [lemma, in Coq.Logic.ExtensionalityFacts]
FunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
FunctionalChoiceOnInhabitedSet [abbreviation, in Coq.Logic.ChoiceFacts]
FunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
FunctionalChoice_on_rel [definition, in Coq.Logic.ChoiceFacts]
FunctionalCountableChoice [abbreviation, in Coq.Logic.ChoiceFacts]
FunctionalCountableChoice_on [definition, in Coq.Logic.ChoiceFacts]
FunctionalDependentChoice [abbreviation, in Coq.Logic.ChoiceFacts]
FunctionalDependentChoice_on [definition, in Coq.Logic.ChoiceFacts]
FunctionalExtensionality [abbreviation, in Coq.Logic.ExtensionalityFacts]
FunctionalExtensionality [library]
FunctionalRelReification [abbreviation, in Coq.Logic.ChoiceFacts]
FunctionalRelReification_on [definition, in Coq.Logic.ChoiceFacts]
functional_extensionality_dep_good__equal_f [lemma, in Coq.Logic.FunctionalExtensionality]
functional_extensionality_dep_good__equal_f_dep [lemma, in Coq.Logic.FunctionalExtensionality]
functional_extensionality_dep_good_refl [lemma, in Coq.Logic.FunctionalExtensionality]
functional_extensionality_dep_good [definition, in Coq.Logic.FunctionalExtensionality]
functional_extensionality [lemma, in Coq.Logic.FunctionalExtensionality]
functional_extensionality_dep [axiom, in Coq.Logic.FunctionalExtensionality]
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
functional_dependent_choice_imp_functional_countable_choice [lemma, in Coq.Logic.ChoiceFacts]
functional_choice_imp_functional_dependent_choice [lemma, in Coq.Logic.ChoiceFacts]
functional_choice_to_inhabited_forall_commute [lemma, in Coq.Logic.ChoiceFacts]
functional_rel_reification_and_rel_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
functional_choice [lemma, in Coq.Logic.IndefiniteDescription]
funct_choice_imp_description [abbreviation, in Coq.Logic.ChoiceFacts]
funct_choice_imp_rel_choice [abbreviation, in Coq.Logic.ChoiceFacts]
FunInd [library]
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_reification_descr_computational_excluded_middle_in_prop_context [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_and_small_drinker_iff_omniscient_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_and_small_drinker_imp_omniscient_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_and_indep_general_prem_iff_guarded_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_and_indep_general_prem_imp_guarded_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_iff_rel_choice_and_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_imp_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
fun_choice_imp_rel_choice [lemma, in Coq.Logic.ChoiceFacts]
fun_if [lemma, in Coq.ssr.ssrbool]
fun_of_simpl [definition, in Coq.ssr.ssrfun]
Further [constructor, in Coq.Lists.Streams]
F_unfold [lemma, in Coq.Program.Wf]
f_equal2_mult [definition, in Coq.Init.Peano]
f_equal2_nat [definition, in Coq.Init.Peano]
f_equal2_plus [definition, in Coq.Init.Peano]
f_equal_pred [definition, in Coq.Init.Peano]
f_equal_nat [definition, in Coq.Init.Peano]
f_eq_dep_non_dep [lemma, in Coq.Logic.EqdepFacts]
f_eq_dep [lemma, in Coq.Logic.EqdepFacts]
f_equal__functional_extensionality_dep_good__fun [definition, in Coq.Logic.FunctionalExtensionality]
f_equal__functional_extensionality_dep_good [definition, in Coq.Logic.FunctionalExtensionality]
F_1_neq_0 [projection, in Coq.setoid_ring.Field_theory]
F_R [projection, in Coq.setoid_ring.Field_theory]
F_push [constructor, in Coq.rtauto.Bintree]
F_empty [constructor, in Coq.rtauto.Bintree]
f_interv_is_interv [lemma, in Coq.Reals.Ranalysis5]
f_incr_implies_g_incr_interv [lemma, in Coq.Reals.Ranalysis5]
f_equal_R [definition, in Coq.Reals.RIneq]
f_equal_compose [lemma, in Coq.Init.Logic]
f_equal5 [lemma, in Coq.Init.Logic]
f_equal4 [lemma, in Coq.Init.Logic]
f_equal3 [lemma, in Coq.Init.Logic]
f_equal2 [lemma, in Coq.Init.Logic]
f_equal_dep2 [lemma, in Coq.Init.Logic]
f_equal_dep [lemma, in Coq.Init.Logic]
f_equal [lemma, in Coq.Init.Logic]
f_adjoint [definition, in Coq.Logic.Adjointification]
f_adjoint_gives_g_adjoint [definition, in Coq.Logic.Adjointification]
f_adjoint_gives_g_adjoint_pointwise [definition, in Coq.Logic.Adjointification]
F1 [constructor, in Coq.Vectors.Fin]
f1 [projection, in Coq.Logic.ClassicalFacts]
f1_o_f2 [projection, in Coq.Logic.ClassicalFacts]
f2 [projection, in Coq.Logic.ClassicalFacts]
F2AF [definition, in Coq.setoid_ring.Field_theory]
| 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 | (25786 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 | (996 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 | (807 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 | (1538 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 | (584 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 | (11835 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 | (956 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 | (627 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 | (306 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 | (475 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 | (493 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 | (903 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 | (1194 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 | (4910 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 | (162 entries) |