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 _ (13565 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 _ (95 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 _ (211 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 _ (305 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 _ (352 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 _ (297 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 _ (183 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 _ (2869 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 _ (287 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)

T

Tactics [library]
Tactics [library]
tail [definition, in Coq.Lists.MonoList]
tail [definition, in Coq.Lists.List]
tail0 [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
tail031 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
tail031_alt [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
tail031_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
tail_mult [definition, in Coq.Arith.Mult]
tail_plus [definition, in Coq.Arith.Plus]
tan [definition, in Coq.Reals.Rtrigo]
tand [definition, in Coq.Reals.Rtrigo_calc]
tanh [definition, in Coq.Reals.Rtrigo_def]
tan_diff [lemma, in Coq.Reals.Rtrigo]
tan_gt_0 [lemma, in Coq.Reals.Rtrigo]
tan_increasing_0 [lemma, in Coq.Reals.Rtrigo]
tan_increasing_1 [lemma, in Coq.Reals.Rtrigo]
tan_incr_0 [lemma, in Coq.Reals.Rtrigo]
tan_incr_1 [lemma, in Coq.Reals.Rtrigo]
tan_lt_0 [lemma, in Coq.Reals.Rtrigo]
tan_minus [lemma, in Coq.Reals.Rtrigo]
tan_neg [lemma, in Coq.Reals.Rtrigo]
tan_PI [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI3 [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI4 [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI6 [lemma, in Coq.Reals.Rtrigo_calc]
tan_plus [lemma, in Coq.Reals.Rtrigo]
tan_0 [lemma, in Coq.Reals.Rtrigo]
tan_2a [lemma, in Coq.Reals.Rtrigo]
tan_2PI [lemma, in Coq.Reals.Rtrigo_calc]
tan_2PI3 [lemma, in Coq.Reals.Rtrigo_calc]
tech1 [lemma, in Coq.Reals.PartSum]
tech10 [lemma, in Coq.Reals.SeqProp]
tech11 [lemma, in Coq.Reals.PartSum]
tech12 [lemma, in Coq.Reals.PartSum]
tech13 [lemma, in Coq.Reals.SeqProp]
tech2 [lemma, in Coq.Reals.PartSum]
tech3 [lemma, in Coq.Reals.PartSum]
tech4 [lemma, in Coq.Reals.PartSum]
tech5 [lemma, in Coq.Reals.PartSum]
tech6 [lemma, in Coq.Reals.PartSum]
tech7 [lemma, in Coq.Reals.PartSum]
tech8 [lemma, in Coq.Reals.ArithProp]
tech9 [lemma, in Coq.Reals.SeqProp]
tech_limit [lemma, in Coq.Reals.Rlimit]
tech_limit_contr [lemma, in Coq.Reals.Rlimit]
tech_pow_Rmult [lemma, in Coq.Reals.Rfunctions]
tech_pow_Rplus [lemma, in Coq.Reals.Rfunctions]
tech_Rgt_minus [lemma, in Coq.Reals.RIneq]
tech_Rplus [lemma, in Coq.Reals.RIneq]
tech_single_z_r_R1 [lemma, in Coq.Reals.RIneq]
tech_up [lemma, in Coq.Reals.R_Ifp]
ternary_operation [definition, in Coq.Classes.RelationClasses]
test_field [definition, in Coq.QArith.Qcanon]
tg_alt [definition, in Coq.Reals.AltSeries]
TheoryList [library]
the_end_of_the_section [constructor, in Coq.Program.Equality]
The_power_set_partial_order [section, in Coq.Sets.Powerset]
The_power_set_partial_order.U [variable, in Coq.Sets.Powerset]
this [projection, in Coq.QArith.Qcanon]
Tl [lemma, in Coq.Lists.TheoryList]
tl [definition, in Coq.Lists.Streams]
tl_nth_tl [lemma, in Coq.Lists.Streams]
Tn [definition, in Coq.Numbers.Cyclic.Int31.Int31]
tn1_step [constructor, in Coq.Relations.Relation_Operators]
tn1_trans [lemma, in Coq.Relations.Operators_Properties]
tn1_trans [constructor, in Coq.Relations.Relation_Operators]
tn1_trans_equiv [lemma, in Coq.Relations.Operators_Properties]
toDeg [definition, in Coq.Reals.Rtrigo_calc]
toRad [definition, in Coq.Reals.Rtrigo_calc]
toRad_inj [lemma, in Coq.Reals.Rtrigo_calc]
Totally_ordered [inductive, in Coq.Sets.Cpo]
Totally_ordered_definition [constructor, in Coq.Sets.Cpo]
total_order_T [axiom, in Coq.Reals.Raxioms]
to_Z [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
to_Z_div_minus_p [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
transitive [definition, in Coq.Relations.Relation_Definitions]
Transitive [definition, in Coq.Sets.Relations_1]
Transitive [record, in Coq.Classes.RelationClasses]
Transitive [inductive, in Coq.Classes.RelationClasses]
Transitive_Closure [section, in Coq.Relations.Relation_Operators]
Transitive_Closure [library]
Transitive_Closure.A [variable, in Coq.Relations.Relation_Operators]
Transitive_Closure.R [variable, in Coq.Relations.Relation_Operators]
transitivity [projection, in Coq.Classes.RelationClasses]
transitivity [constructor, in Coq.Classes.RelationClasses]
translation_0 [lemma, in Coq.Reals.Rgeom]
transp [definition, in Coq.Relations.Relation_Operators]
transpose [definition, in Coq.Lists.SetoidList]
transpose_restr [definition, in Coq.Lists.SetoidList]
trans_clos [abbreviation, in Coq.Wellfounded.Transitive_Closure]
trans_contra_co_morphism [instance, in Coq.Classes.Morphisms]
trans_contra_inv_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_co_eq_inv_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_co_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_eq [lemma, in Coq.Init.Logic]
trans_EqSt [lemma, in Coq.Lists.Streams]
trans_equal [definition, in Coq.Init.Logic]
trans_eq_bool [lemma, in Coq.Bool.Bool]
trans_id [lemma, in Coq.Init.Logic_Type]
trans_JMeq [lemma, in Coq.Logic.JMeq]
trans_rtn1 [lemma, in Coq.Relations.Operators_Properties]
trans_rt1n [lemma, in Coq.Relations.Operators_Properties]
trans_sym_contra_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_sym_co_inv_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_sym_eq [lemma, in Coq.Logic.Eqdep_dec]
trans_tn1 [lemma, in Coq.Relations.Operators_Properties]
trans_t1n [lemma, in Coq.Relations.Operators_Properties]
Tree [inductive, in Coq.Sorting.Heap]
treesort [lemma, in Coq.Sorting.Heap]
treesort_twist1 [lemma, in Coq.Sets.Multiset]
treesort_twist1 [lemma, in Coq.Sets.Uniset]
treesort_twist2 [lemma, in Coq.Sets.Uniset]
treesort_twist2 [lemma, in Coq.Sets.Multiset]
Tree_Leaf [constructor, in Coq.Sorting.Heap]
Tree_Node [constructor, in Coq.Sorting.Heap]
triangle [lemma, in Coq.Reals.Rgeom]
triangle_rectangle [lemma, in Coq.Reals.R_sqr]
triangle_rectangle_le [lemma, in Coq.Reals.R_sqr]
triangle_rectangle_lt [lemma, in Coq.Reals.R_sqr]
Triple [inductive, in Coq.Sets.Ensembles]
Triple_as_Couple [lemma, in Coq.Sets.Powerset_facts]
Triple_as_Couple_Singleton [lemma, in Coq.Sets.Powerset_facts]
Triple_as_union [lemma, in Coq.Sets.Powerset_facts]
Triple_l [constructor, in Coq.Sets.Ensembles]
Triple_m [constructor, in Coq.Sets.Ensembles]
Triple_r [constructor, in Coq.Sets.Ensembles]
triv_nat [lemma, in Coq.Sets.Integers]
True [inductive, in Coq.Init.Logic]
true [constructor, in Coq.Init.Datatypes]
trueP [constructor, in Coq.Logic.ClassicalFacts]
TrueP [definition, in Coq.Logic.ClassicalFacts]
true_predicate [definition, in Coq.Classes.RelationClasses]
true_xorb [abbreviation, in Coq.Bool.Bool]
try_find [definition, in Coq.Lists.TheoryList]
Try_find [lemma, in Coq.Lists.TheoryList]
tt [constructor, in Coq.Init.Datatypes]
twice [definition, in Coq.Numbers.Cyclic.Int31.Int31]
twice_or_twice_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
twice_plus_one [definition, in Coq.Numbers.Cyclic.Int31.Int31]
twice_zero [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
twist [lemma, in Coq.Sets.Permut]
Twon [definition, in Coq.Numbers.Cyclic.Int31.Int31]
two_compl_to_Z_to_two_compl [lemma, in Coq.ZArith.Zbinary]
two_compl_value [lemma, in Coq.ZArith.Zbinary]
two_compl_value_Sn [lemma, in Coq.ZArith.Zbinary]
two_or_two_plus_one [lemma, in Coq.ZArith.Zcomplements]
two_p [definition, in Coq.ZArith.Zpower]
two_power_nat [definition, in Coq.ZArith.Zpower]
two_power_nat_correct [lemma, in Coq.ZArith.Zpower]
two_power_nat_S [lemma, in Coq.ZArith.Zpower]
two_power_pos [definition, in Coq.ZArith.Zpower]
two_power_pos_correct [lemma, in Coq.ZArith.Zpower]
two_power_pos_is_exp [lemma, in Coq.ZArith.Zpower]
two_power_pos_nat [lemma, in Coq.ZArith.Zpower]
two_p_gt_ZERO [lemma, in Coq.ZArith.Zpower]
two_p_is_exp [lemma, in Coq.ZArith.Zpower]
two_p_power2 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
two_p_pred [lemma, in Coq.ZArith.Zpower]
two_p_S [lemma, in Coq.ZArith.Zpower]
Type_with_equality [section, in Coq.Lists.SetoidList]
Type_with_equality.A [variable, in Coq.Lists.SetoidList]
Type_with_equality.eqA [variable, in Coq.Lists.SetoidList]
Type_with_equality.eqA_ltA [variable, in Coq.Lists.SetoidList]
Type_with_equality.eqA_refl [variable, in Coq.Lists.SetoidList]
Type_with_equality.eqA_sym [variable, in Coq.Lists.SetoidList]
Type_with_equality.eqA_trans [variable, in Coq.Lists.SetoidList]
Type_with_equality.EqlistA [section, in Coq.Lists.SetoidList]
Type_with_equality.Filter [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold.B [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Comp [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.eqB [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.f [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.i [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Remove [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Remove.eqA_dec [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Restriction [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Restriction.R [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Restriction.R_compat [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Restriction.R_sym [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Restriction.TraR [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.st [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Tra [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA_eqA [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA_not_eqA [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA_trans [variable, in Coq.Lists.SetoidList]
Type_with_equality.NoDupA [section, in Coq.Lists.SetoidList]
t1n_step [constructor, in Coq.Relations.Relation_Operators]
t1n_trans [lemma, in Coq.Relations.Operators_Properties]
t1n_trans [constructor, in Coq.Relations.Relation_Operators]
t1n_trans_equiv [lemma, in Coq.Relations.Operators_Properties]
T31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
t_step [constructor, in Coq.Relations.Relation_Operators]
t_trans [constructor, in Coq.Relations.Relation_Operators]



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 _ (13565 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 _ (95 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 _ (211 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 _ (305 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 _ (352 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 _ (297 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 _ (183 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 _ (2869 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 _ (287 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)