Standard Library | The Coq Proof Assistant

Global Index

(26016 entries)

Notation Index

F

J

K

T

X

Y

_

(1003 entries)

Module Index

J

X

Y

_

other

(811 entries)

Variable Index

J

Q

V

X

Y

_

other

(1771 entries)

Library Index

K

X

Y

_

other

(588 entries)

Constructor Index

K

Y

_

other

(961 entries)

Lemma Index

other

(11981 entries)

Axiom Index

J

K

V

X

Y

_

other

(508 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

X

Y

_

other

(479 entries)

Section Index

J

Q

X

Y

_

other

(496 entries)

Instance Index

J

V

X

Y

_

other

(905 entries)

Abbreviation Index

J

Y

_

other

(1199 entries)

Definition Index

_

other

(4840 entries)

Record Index

J

X

Y

_

other

(166 entries)

T (lemma)

tail00_spec [in Stdlib.Numbers.Cyclic.Int63.Uint63]
take_prf_irr [in Stdlib.Vectors.VectorSpec]
take_app [in Stdlib.Vectors.VectorSpec]
take_idem [in Stdlib.Vectors.VectorSpec]
take_O [in Stdlib.Vectors.VectorSpec]
tan_pi_plus [in Stdlib.Reals.Rtrigo_facts]
tan_pi_minus [in Stdlib.Reals.Rtrigo_facts]
tan_cos_opp [in Stdlib.Reals.Rtrigo_facts]
tan_cos [in Stdlib.Reals.Rtrigo_facts]
tan_sin_opp [in Stdlib.Reals.Rtrigo_facts]
tan_sin [in Stdlib.Reals.Rtrigo_facts]
tan_acos [in Stdlib.Reals.Ratan]
tan_asin [in Stdlib.Reals.Ratan]
tan_atan [in Stdlib.Reals.Ratan]
tan_1_gt_1 [in Stdlib.Reals.Ratan]
tan_inj [in Stdlib.Reals.Ratan]
tan_increasing [in Stdlib.Reals.Ratan]
tan_2PI3 [in Stdlib.Reals.Rtrigo_calc]
tan_PI3 [in Stdlib.Reals.Rtrigo_calc]
tan_PI6 [in Stdlib.Reals.Rtrigo_calc]
tan_PI4 [in Stdlib.Reals.Rtrigo_calc]
tan_2PI [in Stdlib.Reals.Rtrigo_calc]
tan_PI [in Stdlib.Reals.Rtrigo_calc]
tan_incr_1 [in Stdlib.Reals.Rtrigo1]
tan_incr_0 [in Stdlib.Reals.Rtrigo1]
tan_increasing_1 [in Stdlib.Reals.Rtrigo1]
tan_increasing_0 [in Stdlib.Reals.Rtrigo1]
tan_diff [in Stdlib.Reals.Rtrigo1]
tan_lt_0 [in Stdlib.Reals.Rtrigo1]
tan_gt_0 [in Stdlib.Reals.Rtrigo1]
tan_minus [in Stdlib.Reals.Rtrigo1]
tan_neg [in Stdlib.Reals.Rtrigo1]
tan_0 [in Stdlib.Reals.Rtrigo1]
tan_2a [in Stdlib.Reals.Rtrigo1]
tan_plus [in Stdlib.Reals.Rtrigo1]
tauto_checker_sound [in Stdlib.micromega.Tauto]
tearing_sequences_ordered_forall [in Stdlib.Reals.Runcountable]
tearing_sequences_inc_dec [in Stdlib.Reals.Runcountable]
tearing_sequences_projsig [in Stdlib.Reals.Runcountable]
tech [in Stdlib.Reals.Machin]
tech_up [in Stdlib.Reals.R_Ifp]
tech_opp_tan [in Stdlib.Reals.Ratan]
tech_single_z_r_R1_depr [in Stdlib.Reals.RIneq]
tech_limit_contr [in Stdlib.Reals.Rlimit]
tech_limit [in Stdlib.Reals.Rlimit]
tech_pow_Rplus [in Stdlib.Reals.Rfunctions]
tech_pow_Rmult [in Stdlib.Reals.Rfunctions]
tech1 [in Stdlib.Reals.PartSum]
tech11 [in Stdlib.Reals.PartSum]
tech12 [in Stdlib.Reals.PartSum]
tech13 [in Stdlib.Reals.SeqProp]
tech2 [in Stdlib.Reals.PartSum]
tech3 [in Stdlib.Reals.PartSum]
tech4 [in Stdlib.Reals.PartSum]
tech5 [in Stdlib.Reals.PartSum]
tech6 [in Stdlib.Reals.PartSum]
tech7 [in Stdlib.Reals.PartSum]
tech8 [in Stdlib.Reals.ArithProp]
tech9 [in Stdlib.Reals.SeqProp]
Tget_Tmap [in Stdlib.rtauto.Bintree]
Tget_Tadd [in Stdlib.rtauto.Bintree]
Tget_Tempty [in Stdlib.rtauto.Bintree]
tl_nth_tl [in Stdlib.Lists.Streams]
Tmap_Tadd [in Stdlib.rtauto.Bintree]
TOMaxEqDec_to_Compare.compare_spec [in Stdlib.Structures.GenericMinMax]
topredE [in Stdlib.ssr.ssrbool]
toRad_inj [in Stdlib.Reals.Rtrigo_calc]
torn_number_below_second_sequence [in Stdlib.Reals.Runcountable]
torn_number_above_first_sequence [in Stdlib.Reals.Runcountable]
total_order_T [in Stdlib.Reals.Rdefinitions]
to_Z_abs [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_opp [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_pred [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_succ [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_mul [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_sub [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_add [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_cmodwB [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_mod_Uint63to_Z [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_inj [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_bounded [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_max [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_min [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_Z_0 [in Stdlib.Numbers.Cyclic.Int63.Sint63]
to_pos_of_pos [in Stdlib.Strings.BinaryString]
to_nat_of_nat [in Stdlib.Strings.BinaryString]
to_N_of_N [in Stdlib.Strings.BinaryString]
to_list_cat [in Stdlib.Strings.PString]
to_list_firstn_skipn_middle [in Stdlib.Strings.PString]
to_of_list [in Stdlib.Strings.PString]
to_list_inj [in Stdlib.Strings.PString]
to_list_inj [in Stdlib.Numbers.HexadecimalFacts]
to_list_of_list [in Stdlib.Numbers.HexadecimalFacts]
to_decimal_surj [in Stdlib.Numbers.DecimalR]
to_decimal_inj [in Stdlib.Numbers.DecimalR]
to_of [in Stdlib.Numbers.DecimalR]
to_list_Forall2 [in Stdlib.Vectors.VectorSpec]
to_list_In [in Stdlib.Vectors.VectorSpec]
to_list_Exists [in Stdlib.Vectors.VectorSpec]
to_list_Forall [in Stdlib.Vectors.VectorSpec]
to_list_fold_right [in Stdlib.Vectors.VectorSpec]
to_list_fold_left [in Stdlib.Vectors.VectorSpec]
to_list_map [in Stdlib.Vectors.VectorSpec]
to_list_rev [in Stdlib.Vectors.VectorSpec]
to_list_rev_append [in Stdlib.Vectors.VectorSpec]
to_list_rev_append_tail [in Stdlib.Vectors.VectorSpec]
to_list_append [in Stdlib.Vectors.VectorSpec]
to_list_tl [in Stdlib.Vectors.VectorSpec]
to_list_nth_order [in Stdlib.Vectors.VectorSpec]
to_list_const [in Stdlib.Vectors.VectorSpec]
to_list_last [in Stdlib.Vectors.VectorSpec]
to_list_hd [in Stdlib.Vectors.VectorSpec]
to_list_inj [in Stdlib.Vectors.VectorSpec]
to_list_nil_iff [in Stdlib.Vectors.VectorSpec]
to_list_cons [in Stdlib.Vectors.VectorSpec]
to_list_nil [in Stdlib.Vectors.VectorSpec]
to_list_of_list_opp [in Stdlib.Vectors.VectorSpec]
to_nat_inj [in Stdlib.Vectors.Fin]
to_nat_of_nat [in Stdlib.Vectors.Fin]
to_int_surj [in Stdlib.Numbers.HexadecimalZ]
to_int_inj [in Stdlib.Numbers.HexadecimalZ]
to_of [in Stdlib.Numbers.HexadecimalZ]
to_decimal_surj [in Stdlib.Numbers.DecimalQ]
to_decimal_inj [in Stdlib.Numbers.DecimalQ]
to_of [in Stdlib.Numbers.DecimalQ]
to_pos_of_pos [in Stdlib.Strings.HexString]
to_nat_of_nat [in Stdlib.Strings.HexString]
to_Z_of_Z [in Stdlib.Strings.HexString]
to_N_of_N [in Stdlib.Strings.HexString]
to_hexadecimal_surj [in Stdlib.Numbers.HexadecimalR]
to_hexadecimal_inj [in Stdlib.Numbers.HexadecimalR]
to_of [in Stdlib.Numbers.HexadecimalR]
to_hexadecimal_surj [in Stdlib.Numbers.HexadecimalQ]
to_hexadecimal_inj [in Stdlib.Numbers.HexadecimalQ]
to_of [in Stdlib.Numbers.HexadecimalQ]
to_nat_via_N [in Stdlib.Strings.Byte]
to_N_via_nat [in Stdlib.Strings.Byte]
to_N_bounded [in Stdlib.Strings.Byte]
to_of_N_option_map [in Stdlib.Strings.Byte]
to_of_N_iff [in Stdlib.Strings.Byte]
to_of_N [in Stdlib.Strings.Byte]
to_nat_bounded [in Stdlib.Strings.Byte]
to_of_nat_option_map [in Stdlib.Strings.Byte]
to_of_nat_iff [in Stdlib.Strings.Byte]
to_of_nat [in Stdlib.Strings.Byte]
to_Z_bounded [in Stdlib.micromega.ZifyUint63]
to_bits_of_bits [in Stdlib.Init.Byte]
to_pos_of_pos [in Stdlib.Strings.OctalString]
to_nat_of_nat [in Stdlib.Strings.OctalString]
to_Z_of_Z [in Stdlib.Strings.OctalString]
to_N_of_N [in Stdlib.Strings.OctalString]
to_list_inj [in Stdlib.Numbers.DecimalFacts]
to_list_of_list [in Stdlib.Numbers.DecimalFacts]
to_int_surj [in Stdlib.Numbers.DecimalZ]
to_int_inj [in Stdlib.Numbers.DecimalZ]
to_of [in Stdlib.Numbers.DecimalZ]
to_nat_non_decreasing [in Stdlib.Arith.Cantor]
to_nat_spec2 [in Stdlib.Arith.Cantor]
to_nat_spec [in Stdlib.Arith.Cantor]
to_nat_inj [in Stdlib.Arith.Cantor]
to_Z_bounded [in Stdlib.micromega.ZifySint63]
to_Z_split [in Stdlib.Numbers.Cyclic.Int63.Uint63]
to_Z_gcd [in Stdlib.Numbers.Cyclic.Int63.Uint63]
to_Z_inj [in Stdlib.Numbers.Cyclic.Int63.Uint63]
to_Z_1 [in Stdlib.Numbers.Cyclic.Int63.Uint63]
to_Z_0 [in Stdlib.Numbers.Cyclic.Int63.Uint63]
to_Z_bounded [in Stdlib.Numbers.Cyclic.Int63.Uint63]
to_Z_rec_bounded [in Stdlib.Numbers.Cyclic.Int63.Uint63]
translation_0 [in Stdlib.Reals.Rgeom]
trans_EqSt [in Stdlib.Lists.Streams]
trans_eq_bool [in Stdlib.Bool.Bool]
trans_sym_eq [in Stdlib.Logic.Eqdep_dec]
treesort [in Stdlib.Sorting.Heap]
treesort_twist2 [in Stdlib.Sets.Uniset]
treesort_twist1 [in Stdlib.Sets.Uniset]
treesort_twist2 [in Stdlib.Sets.Multiset]
treesort_twist1 [in Stdlib.Sets.Multiset]
triangle [in Stdlib.Reals.Rgeom]
triangle_rectangle_le [in Stdlib.Reals.R_sqr]
triangle_rectangle_lt [in Stdlib.Reals.R_sqr]
triangle_rectangle [in Stdlib.Reals.R_sqr]
Triple_as_Couple_Singleton [in Stdlib.Sets.Powerset_facts]
Triple_as_Couple [in Stdlib.Sets.Powerset_facts]
Triple_as_union [in Stdlib.Sets.Powerset_facts]
triv_nat [in Stdlib.Sets.Integers]
triv_div_th [in Stdlib.setoid_ring.InitialRing]
true_hprop [in Stdlib.Logic.HLevels]
trunc [in Stdlib.Vectors.VectorDef]
TTLB_to_OTF.le_lteq [in Stdlib.Structures.Orders]
TTLB_to_OTF.eqb_eq [in Stdlib.Structures.Orders]
TTLB_to_OTF.compare_spec [in Stdlib.Structures.Orders]
twist [in Stdlib.Sets.Permut]
two_p_pred [in Stdlib.ZArith.Zpower]
two_p_S [in Stdlib.ZArith.Zpower]
two_p_gt_ZERO [in Stdlib.ZArith.Zpower]
two_p_is_exp [in Stdlib.ZArith.Zpower]
two_p_correct [in Stdlib.ZArith.Zpower]
two_power_pos_is_exp [in Stdlib.ZArith.Zpower]
two_power_pos_correct [in Stdlib.ZArith.Zpower]
two_power_pos_nat [in Stdlib.ZArith.Zpower]
two_power_nat_correct [in Stdlib.ZArith.Zpower]
two_power_nat_S [in Stdlib.ZArith.Zpower]
two_p_equiv [in Stdlib.ZArith.Zpower]
two_power_pos_equiv [in Stdlib.ZArith.Zpower]
two_power_nat_equiv [in Stdlib.ZArith.Zpower]
TypeNeqSmallType.paradox [in Stdlib.Logic.Hurkens]
TypeNeqSmallType.up_down [in Stdlib.Logic.Hurkens]

Global Index

(26016 entries)

Notation Index

F

J

K

T

X

Y

_

(1003 entries)

Module Index

J

X

Y

_

other

(811 entries)

Variable Index

J

Q

V

X

Y

_

other

(1771 entries)

Library Index

K

X

Y

_

other

(588 entries)

Constructor Index

K

Y

_

other

(961 entries)

Lemma Index

other

(11981 entries)

Axiom Index

J

K

V

X

Y

_

other

(508 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

X

Y

_

other

(479 entries)

Section Index

J

Q

X

Y

_

other

(496 entries)

Instance Index

J

V

X

Y

_

other

(905 entries)

Abbreviation Index

J

Y

_

other

(1199 entries)

Definition Index

_

other

(4840 entries)

Record Index

J

X

Y

_

other

(166 entries)