| 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 | (23166 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 | (950 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 | (746 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 | (1491 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 | (545 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 | (10708 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 | (946 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 | (603 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 | (461 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 | (291 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 | (473 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 | (760 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 | (1145 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 | (3885 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) |
T
t [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]t [inductive, in Coq.Vectors.Fin]
t [definition, in Coq.Init.Nat]
t [abbreviation, in Coq.micromega.VarMap]
t [inductive, in Coq.micromega.VarMap]
t [inductive, in Coq.Vectors.VectorDef]
Tactics [library]
Tactics [library]
tactic_view [constructor, in Coq.ssr.ssreflect]
Tadd [definition, in Coq.rtauto.Bintree]
tag [definition, in Coq.ssr.ssrfun]
Tag [section, in Coq.ssr.ssrfun]
Tagged [definition, in Coq.ssr.ssrfun]
tagged [definition, in Coq.ssr.ssrfun]
Tagged2 [definition, in Coq.ssr.ssrfun]
tagged2 [definition, in Coq.ssr.ssrfun]
tagged2' [definition, in Coq.ssr.ssrfun]
tag_of_sig [definition, in Coq.ssr.ssrfun]
tag_of_tag2 [definition, in Coq.ssr.ssrfun]
Tag.i [variable, in Coq.ssr.ssrfun]
Tag.I [variable, in Coq.ssr.ssrfun]
Tag.T_ [variable, in Coq.ssr.ssrfun]
Tag.U_ [variable, in Coq.ssr.ssrfun]
tag2 [definition, in Coq.ssr.ssrfun]
tail [definition, in Coq.micromega.Env]
tail [abbreviation, in Coq.Lists.List]
tail_mult [definition, in Coq.Arith.Mult]
tail_mul [definition, in Coq.Init.Nat]
tail_addmul [definition, in Coq.Init.Nat]
tail_add [definition, in Coq.Init.Nat]
tail_plus [definition, in Coq.Arith.Plus]
tail0 [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
tail0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
tail0_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
tail00_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
tail031 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
tail031_equiv [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
tail031_alt [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
take [definition, in Coq.Vectors.VectorDef]
take_prf_irr [lemma, in Coq.Vectors.VectorSpec]
take_app [lemma, in Coq.Vectors.VectorSpec]
take_idem [lemma, in Coq.Vectors.VectorSpec]
take_O [lemma, in Coq.Vectors.VectorSpec]
tan [definition, in Coq.Reals.Rtrigo1]
tand [definition, in Coq.Reals.Rtrigo_calc]
tanh [definition, in Coq.Reals.Rtrigo_def]
tan_2PI3 [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI3 [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI6 [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI4 [lemma, in Coq.Reals.Rtrigo_calc]
tan_2PI [lemma, in Coq.Reals.Rtrigo_calc]
tan_PI [lemma, in Coq.Reals.Rtrigo_calc]
tan_incr_1 [lemma, in Coq.Reals.Rtrigo1]
tan_incr_0 [lemma, in Coq.Reals.Rtrigo1]
tan_increasing_1 [lemma, in Coq.Reals.Rtrigo1]
tan_increasing_0 [lemma, in Coq.Reals.Rtrigo1]
tan_diff [lemma, in Coq.Reals.Rtrigo1]
tan_lt_0 [lemma, in Coq.Reals.Rtrigo1]
tan_gt_0 [lemma, in Coq.Reals.Rtrigo1]
tan_minus [lemma, in Coq.Reals.Rtrigo1]
tan_neg [lemma, in Coq.Reals.Rtrigo1]
tan_0 [lemma, in Coq.Reals.Rtrigo1]
tan_2a [lemma, in Coq.Reals.Rtrigo1]
tan_plus [lemma, in Coq.Reals.Rtrigo1]
tan_1_gt_1 [lemma, in Coq.Reals.Ratan]
tan_is_inj [lemma, in Coq.Reals.Ratan]
tan_increasing [lemma, in Coq.Reals.Ratan]
target [projection, in Coq.micromega.ZifyClasses]
target_prop [projection, in Coq.micromega.ZifyClasses]
Tauto [library]
Tauto [library]
tauto_checker_sound [lemma, in Coq.micromega.Tauto]
tauto_checker [definition, in Coq.micromega.Tauto]
TBOp [projection, in Coq.micromega.ZifyClasses]
TBOpInj [projection, in Coq.micromega.ZifyClasses]
Tcons [constructor, in Coq.Classes.RelationClasses]
TCst [projection, in Coq.micromega.ZifyClasses]
TCstInj [projection, in Coq.micromega.ZifyClasses]
tearing_elem_fst [definition, in Coq.Reals.Runcountable]
tearing_sequences_ordered_forall [lemma, in Coq.Reals.Runcountable]
tearing_sequences_inc_dec [lemma, in Coq.Reals.Runcountable]
tearing_sequences_projsig [lemma, in Coq.Reals.Runcountable]
tearing_sequences [definition, in Coq.Reals.Runcountable]
tech [lemma, in Coq.Reals.Machin]
tech_single_z_r_R1 [lemma, in Coq.Reals.RIneq]
tech_Rgt_minus [lemma, in Coq.Reals.RIneq]
tech_Rplus [lemma, in Coq.Reals.RIneq]
tech_up [lemma, in Coq.Reals.R_Ifp]
tech_limit_contr [lemma, in Coq.Reals.Rlimit]
tech_limit [lemma, in Coq.Reals.Rlimit]
tech_pow_Rplus [lemma, in Coq.Reals.Rfunctions]
tech_pow_Rmult [lemma, in Coq.Reals.Rfunctions]
tech_opp_tan [lemma, in Coq.Reals.Ratan]
tech1 [lemma, in Coq.Reals.PartSum]
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]
Tempty [constructor, in Coq.rtauto.Bintree]
ten [abbreviation, in Coq.Init.Nat]
ternary_operation [definition, in Coq.Classes.RelationClasses]
testbit [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit [definition, in Coq.Init.Nat]
testbit_bitwise_2 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit_bitwise_1 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit_even_succ [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit_odd_succ [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit_even_0 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit_odd_0 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
testbit_0_l [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
TestOrder [section, in Coq.Numbers.Integer.Binary.ZBinary]
TestOrder [section, in Coq.NArith.NArith]
TestOrder [section, in Coq.Arith.PeanoNat]
TestOrder.test [variable, in Coq.Numbers.Integer.Binary.ZBinary]
TestOrder.test [variable, in Coq.NArith.NArith]
TestOrder.test [variable, in Coq.Arith.PeanoNat]
TestRing [section, in Coq.Numbers.Cyclic.Int63.Ring63]
TestRing [section, in Coq.Numbers.Cyclic.Int31.Ring31]
TestRing.test [variable, in Coq.Numbers.Cyclic.Int63.Ring63]
TestRing.test [variable, in Coq.Numbers.Cyclic.Int31.Ring31]
test_field [definition, in Coq.QArith.Qcanon]
TFormula [definition, in Coq.micromega.Tauto]
Tget [definition, in Coq.rtauto.Bintree]
Tget_Tmap [lemma, in Coq.rtauto.Bintree]
Tget_Tadd [lemma, in Coq.rtauto.Bintree]
Tget_Tempty [lemma, in Coq.rtauto.Bintree]
tg_alt [definition, in Coq.Reals.AltSeries]
TheCanonical [module, in Coq.ssr.ssreflect]
TheCanonical.get [definition, in Coq.ssr.ssreflect]
TheCanonical.get_by [definition, in Coq.ssr.ssreflect]
TheCanonical.Put [constructor, in Coq.ssr.ssreflect]
TheCanonical.put [inductive, in Coq.ssr.ssreflect]
The_power_set_partial_order.U [variable, in Coq.Sets.Powerset]
The_power_set_partial_order [section, in Coq.Sets.Powerset]
this [projection, in Coq.QArith.Qcanon]
tl [definition, in Coq.Lists.Streams]
tl [definition, in Coq.Vectors.VectorDef]
tl [definition, in Coq.Lists.List]
Tlist [inductive, in Coq.Classes.RelationClasses]
tl_nth_tl [lemma, in Coq.Lists.Streams]
Tmap [definition, in Coq.rtauto.Bintree]
Tmap_Tadd [lemma, in Coq.rtauto.Bintree]
Tn [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Tnil [constructor, in Coq.Classes.RelationClasses]
tn1_trans_equiv [abbreviation, in Coq.Relations.Operators_Properties]
tn1_trans [abbreviation, in Coq.Relations.Operators_Properties]
tn1_trans [constructor, in Coq.Relations.Relation_Operators]
tn1_step [constructor, in Coq.Relations.Relation_Operators]
toDeg [definition, in Coq.Reals.Rtrigo_calc]
TOMaxEqDec_to_OTF [module, in Coq.Structures.GenericMinMax]
TOMaxEqDec_to_Compare.compare_spec [lemma, in Coq.Structures.GenericMinMax]
TOMaxEqDec_to_Compare.compare [definition, in Coq.Structures.GenericMinMax]
TOMaxEqDec_to_Compare [module, in Coq.Structures.GenericMinMax]
topred [projection, in Coq.ssr.ssrbool]
topredE [lemma, in Coq.ssr.ssrbool]
toRad [definition, in Coq.Reals.Rtrigo_calc]
toRad_inj [lemma, in Coq.Reals.Rtrigo_calc]
torn_number_below_second_sequence [lemma, in Coq.Reals.Runcountable]
torn_number_above_first_sequence [lemma, in Coq.Reals.Runcountable]
torn_number [definition, in Coq.Reals.Runcountable]
total [definition, in Coq.ssr.ssrbool]
TotalLeBool [module, in Coq.Structures.Orders]
TotalLeBool' [module, in Coq.Structures.Orders]
Totally_ordered_definition [constructor, in Coq.Sets.Cpo]
Totally_ordered [inductive, in Coq.Sets.Cpo]
TotalOrder [module, in Coq.Structures.Orders]
TotalOrder' [module, in Coq.Structures.Orders]
TotalTransitiveLeBool [module, in Coq.Structures.Orders]
TotalTransitiveLeBool' [module, in Coq.Structures.Orders]
total_order_T [lemma, in Coq.Reals.Rdefinitions]
to_list_of_list_opp [lemma, in Coq.Vectors.VectorSpec]
to_nat [abbreviation, in Coq.micromega.RMicromega]
to_Z_split [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_gcd [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_inj [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_1 [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_0 [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_rec_bounded [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z [definition, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z_rec [definition, in Coq.Numbers.Cyclic.Int63.Int63]
to_Z [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
to_pos_of_pos [lemma, in Coq.Strings.BinaryString]
to_nat_of_nat [lemma, in Coq.Strings.BinaryString]
to_N_of_N [lemma, in Coq.Strings.BinaryString]
to_nat [definition, in Coq.Strings.BinaryString]
to_Z [definition, in Coq.Strings.BinaryString]
to_pos [definition, in Coq.Strings.BinaryString]
to_N [definition, in Coq.Strings.BinaryString]
to_bits_of_bits [lemma, in Coq.Init.Byte]
to_bits [definition, in Coq.Init.Byte]
to_nat_inj [lemma, in Coq.Vectors.Fin]
to_nat_of_nat [lemma, in Coq.Vectors.Fin]
to_nat [definition, in Coq.Vectors.Fin]
to_int [definition, in Coq.Init.Nat]
to_uint [definition, in Coq.Init.Nat]
to_little_uint [definition, in Coq.Init.Nat]
to_pos_of_pos [lemma, in Coq.Strings.OctalString]
to_nat_of_nat [lemma, in Coq.Strings.OctalString]
to_Z_of_Z [lemma, in Coq.Strings.OctalString]
to_N_of_N [lemma, in Coq.Strings.OctalString]
to_nat [definition, in Coq.Strings.OctalString]
to_Z [definition, in Coq.Strings.OctalString]
to_pos [definition, in Coq.Strings.OctalString]
to_N [definition, in Coq.Strings.OctalString]
to_nat_via_N [lemma, in Coq.Strings.Byte]
to_N_via_nat [lemma, in Coq.Strings.Byte]
to_N_bounded [lemma, in Coq.Strings.Byte]
to_of_N_option_map [lemma, in Coq.Strings.Byte]
to_of_N_iff [lemma, in Coq.Strings.Byte]
to_of_N [lemma, in Coq.Strings.Byte]
to_N [definition, in Coq.Strings.Byte]
to_nat_bounded [lemma, in Coq.Strings.Byte]
to_of_nat_option_map [lemma, in Coq.Strings.Byte]
to_of_nat_iff [lemma, in Coq.Strings.Byte]
to_of_nat [lemma, in Coq.Strings.Byte]
to_nat [definition, in Coq.Strings.Byte]
to_constrT [record, in Coq.micromega.Tauto]
to_pos_of_pos [lemma, in Coq.Strings.HexString]
to_nat_of_nat [lemma, in Coq.Strings.HexString]
to_Z_of_Z [lemma, in Coq.Strings.HexString]
to_N_of_N [lemma, in Coq.Strings.HexString]
to_nat [definition, in Coq.Strings.HexString]
to_Z [definition, in Coq.Strings.HexString]
to_pos [definition, in Coq.Strings.HexString]
to_N [definition, in Coq.Strings.HexString]
to_list [definition, in Coq.Vectors.VectorDef]
to_Bvector [definition, in Coq.Strings.ByteVector]
to_string [definition, in Coq.Strings.ByteVector]
to_decimal [definition, in Coq.QArith.QArith_base]
to_int_surj [lemma, in Coq.Numbers.DecimalZ]
to_int_inj [lemma, in Coq.Numbers.DecimalZ]
to_of [lemma, in Coq.Numbers.DecimalZ]
TR [projection, in Coq.micromega.ZifyClasses]
Transitive [record, in Coq.Classes.CRelationClasses]
Transitive [inductive, in Coq.Classes.CRelationClasses]
transitive [definition, in Coq.ssr.ssrbool]
Transitive [definition, in Coq.Sets.Relations_1]
transitive [definition, in Coq.Relations.Relation_Definitions]
Transitive [record, in Coq.Classes.RelationClasses]
Transitive [inductive, in Coq.Classes.RelationClasses]
Transitive_Closure.R [variable, in Coq.Relations.Relation_Operators]
Transitive_Closure.A [variable, in Coq.Relations.Relation_Operators]
Transitive_Closure [section, in Coq.Relations.Relation_Operators]
Transitive_Closure [library]
transitivity [projection, in Coq.Classes.CRelationClasses]
transitivity [constructor, in Coq.Classes.CRelationClasses]
transitivity [projection, in Coq.Classes.RelationClasses]
transitivity [constructor, in Coq.Classes.RelationClasses]
Translation [section, in Coq.btauto.Reflect]
translation_0 [lemma, in Coq.Reals.Rgeom]
transp [definition, in Coq.Relations.Relation_Operators]
transpose [definition, in Coq.Lists.SetoidList]
transpose_restr2 [definition, in Coq.Lists.SetoidList]
transpose_restr [definition, in Coq.Lists.SetoidList]
transpose2 [definition, in Coq.Lists.SetoidList]
trans_co_eq_inv_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_sym_contra_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_sym_co_inv_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_co_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_contra_inv_impl_morphism [instance, in Coq.Classes.Morphisms]
trans_contra_co_morphism [instance, in Coq.Classes.Morphisms]
trans_EqSt [lemma, in Coq.Lists.Streams]
trans_JMeq [abbreviation, in Coq.Logic.JMeq]
trans_rtn1 [abbreviation, in Coq.Relations.Operators_Properties]
trans_rt1n [abbreviation, in Coq.Relations.Operators_Properties]
trans_t1n [abbreviation, in Coq.Relations.Operators_Properties]
trans_tn1 [abbreviation, in Coq.Relations.Operators_Properties]
trans_equal [abbreviation, in Coq.Init.Logic]
trans_eq [abbreviation, in Coq.Init.Logic]
trans_ord [definition, in Coq.Structures.OrdersTac]
trans_sym_eq [lemma, in Coq.Logic.Eqdep_dec]
trans_clos [abbreviation, in Coq.Wellfounded.Transitive_Closure]
trans_id [abbreviation, in Coq.Init.Logic_Type]
trans_eq_bool [lemma, in Coq.Bool.Bool]
trans_co_eq_inv_arrow_morphism [instance, in Coq.Classes.CMorphisms]
trans_sym_contra_arrow_morphism [instance, in Coq.Classes.CMorphisms]
trans_sym_co_inv_impl_type_morphism [instance, in Coq.Classes.CMorphisms]
trans_co_impl_type_morphism [instance, in Coq.Classes.CMorphisms]
trans_contra_inv_impl_type_morphism [instance, in Coq.Classes.CMorphisms]
trans_contra_co_type_morphism [instance, in Coq.Classes.CMorphisms]
Tree [inductive, in Coq.Sorting.Heap]
Tree [abbreviation, in Coq.rtauto.Bintree]
Tree [inductive, in Coq.rtauto.Bintree]
treesort [lemma, in Coq.Sorting.Heap]
treesort_twist2 [lemma, in Coq.Sets.Multiset]
treesort_twist1 [lemma, in Coq.Sets.Multiset]
treesort_twist2 [lemma, in Coq.Sets.Uniset]
treesort_twist1 [lemma, in Coq.Sets.Uniset]
Tree_Node [constructor, in Coq.Sorting.Heap]
Tree_Leaf [constructor, in Coq.Sorting.Heap]
Tremove [definition, in Coq.rtauto.Bintree]
triangle [lemma, in Coq.Reals.Rgeom]
triangle_rectangle_le [lemma, in Coq.Reals.R_sqr]
triangle_rectangle_lt [lemma, in Coq.Reals.R_sqr]
triangle_rectangle [lemma, in Coq.Reals.R_sqr]
TRInj [projection, in Coq.micromega.ZifyClasses]
Triple [inductive, in Coq.Sets.Ensembles]
Triple_r [constructor, in Coq.Sets.Ensembles]
Triple_m [constructor, in Coq.Sets.Ensembles]
Triple_l [constructor, in Coq.Sets.Ensembles]
Triple_as_Couple_Singleton [lemma, in Coq.Sets.Powerset_facts]
Triple_as_Couple [lemma, in Coq.Sets.Powerset_facts]
Triple_as_union [lemma, in Coq.Sets.Powerset_facts]
triv_nat [lemma, in Coq.Sets.Integers]
triv_div_th [lemma, in Coq.setoid_ring.InitialRing]
triv_div [definition, in Coq.setoid_ring.InitialRing]
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_hprop [lemma, in Coq.Logic.HLevels]
true_xorb [abbreviation, in Coq.Bool.Bool]
trunc [lemma, in Coq.Vectors.VectorDef]
tt [constructor, in Coq.Init.Datatypes]
TT [constructor, in Coq.micromega.Tauto]
TTLB_to_OTF.le_lteq [definition, in Coq.Structures.Orders]
TTLB_to_OTF.lt_compat [instance, in Coq.Structures.Orders]
TTLB_to_OTF.lt_strorder [instance, in Coq.Structures.Orders]
TTLB_to_OTF.eq_equiv [instance, in Coq.Structures.Orders]
TTLB_to_OTF.eqb_eq [lemma, in Coq.Structures.Orders]
TTLB_to_OTF.eqb [definition, in Coq.Structures.Orders]
TTLB_to_OTF.compare_spec [lemma, in Coq.Structures.Orders]
TTLB_to_OTF.compare [definition, in Coq.Structures.Orders]
TTLB_to_OTF.lt [definition, in Coq.Structures.Orders]
TTLB_to_OTF.eq [definition, in Coq.Structures.Orders]
TTLB_to_OTF.le [definition, in Coq.Structures.Orders]
TTLB_to_OTF.t [definition, in Coq.Structures.Orders]
TTLB_to_OTF [module, in Coq.Structures.Orders]
TUOp [projection, in Coq.micromega.ZifyClasses]
TUOpInj [projection, in Coq.micromega.ZifyClasses]
twice [definition, in Coq.Numbers.Cyclic.Int31.Int31]
twice_or_twice_plus_one [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
twice_zero [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
twice_plus_one [definition, in Coq.Numbers.Cyclic.Int31.Int31]
twist [lemma, in Coq.Sets.Permut]
two [definition, in Coq.Init.Nat]
two [definition, in Coq.Floats.PrimFloat]
Twon [definition, in Coq.Numbers.Cyclic.Int31.Int31]
two_p_pred [lemma, in Coq.ZArith.Zpower]
two_p_S [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_correct [lemma, in Coq.ZArith.Zpower]
two_power_pos_is_exp [lemma, in Coq.ZArith.Zpower]
two_power_pos_correct [lemma, in Coq.ZArith.Zpower]
two_power_pos_nat [lemma, in Coq.ZArith.Zpower]
two_power_nat_correct [lemma, in Coq.ZArith.Zpower]
two_power_nat_S [lemma, in Coq.ZArith.Zpower]
two_p_equiv [lemma, in Coq.ZArith.Zpower]
two_power_pos_equiv [lemma, in Coq.ZArith.Zpower]
two_power_nat_equiv [lemma, in Coq.ZArith.Zpower]
two_p [definition, in Coq.ZArith.Zpower]
two_power_pos [definition, in Coq.ZArith.Zpower]
two_power_nat [definition, in Coq.ZArith.Zpower]
two_p_power2 [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
two_or_two_plus_one [abbreviation, in Coq.ZArith.Zcomplements]
two_compl_to_Z_to_two_compl [lemma, in Coq.ZArith.Zdigits]
two_compl_value_Sn [lemma, in Coq.ZArith.Zdigits]
two_compl_value [lemma, in Coq.ZArith.Zdigits]
Typ [module, in Coq.Structures.Equalities]
TypElt [module, in Coq.MSets.MSetInterface]
TypElt.elt [axiom, in Coq.MSets.MSetInterface]
TypElt.t [axiom, in Coq.MSets.MSetInterface]
TypeNeqSmallType [module, in Coq.Logic.Hurkens]
TypeNeqSmallType.paradox [lemma, in Coq.Logic.Hurkens]
TypeNeqSmallType.Paradox [section, in Coq.Logic.Hurkens]
TypeNeqSmallType.Paradox.A [variable, in Coq.Logic.Hurkens]
TypeNeqSmallType.Paradox.down [variable, in Coq.Logic.Hurkens]
TypeNeqSmallType.Paradox.h [variable, in Coq.Logic.Hurkens]
TypeNeqSmallType.Paradox.U [variable, in Coq.Logic.Hurkens]
TypeNeqSmallType.Paradox.up [variable, in Coq.Logic.Hurkens]
TypeNeqSmallType.up_down [lemma, in Coq.Logic.Hurkens]
Type_with_equality.Filter [section, in Coq.Lists.SetoidList]
Type_with_equality.EqlistA [section, in Coq.Lists.SetoidList]
Type_with_equality.sotrans [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA_compat [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA_strorder [variable, in Coq.Lists.SetoidList]
Type_with_equality.ltA [variable, in Coq.Lists.SetoidList]
Type_with_equality.Remove.eqA_dec [variable, in Coq.Lists.SetoidList]
Type_with_equality.Remove [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Tra [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Fold2_With_Restriction.TraR [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Fold2_With_Restriction.R_compat [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Fold2_With_Restriction.R_sym [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Fold2_With_Restriction.R [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Fold2_With_Restriction [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.Comp [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.f [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.st [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.eqB [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2.B [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold2 [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Tra [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Fold_With_Restriction.TraR [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Fold_With_Restriction.R_compat [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Fold_With_Restriction.R_sym [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Fold_With_Restriction.R [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Fold_With_Restriction [section, in Coq.Lists.SetoidList]
Type_with_equality.Fold.Comp [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.i [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.f [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.st [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.eqB [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold.B [variable, in Coq.Lists.SetoidList]
Type_with_equality.Fold [section, in Coq.Lists.SetoidList]
Type_with_equality.EquivlistA [section, in Coq.Lists.SetoidList]
Type_with_equality.NoDupA [section, in Coq.Lists.SetoidList]
Type_with_equality.eqA_equiv [variable, in Coq.Lists.SetoidList]
Type_with_equality.eqA [variable, in Coq.Lists.SetoidList]
Type_with_equality.A [variable, in Coq.Lists.SetoidList]
Type_with_equality [section, in Coq.Lists.SetoidList]
Typ.t [axiom, in Coq.Structures.Equalities]
t_trans [constructor, in Coq.Relations.Relation_Operators]
t_step [constructor, in Coq.Relations.Relation_Operators]
t1n_trans_equiv [abbreviation, in Coq.Relations.Operators_Properties]
t1n_trans [abbreviation, in Coq.Relations.Operators_Properties]
t1n_trans [constructor, in Coq.Relations.Relation_Operators]
t1n_step [constructor, in Coq.Relations.Relation_Operators]
T31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
| 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 | (23166 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 | (950 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 | (746 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 | (1491 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 | (545 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 | (10708 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 | (946 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 | (603 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 | (461 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 | (291 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 | (473 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 | (760 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 | (1145 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 | (3885 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) |