Standard Library | The Coq Proof Assistant

Global Index

(72745 entries)

Notation Index

F

J

K

T

X

Y

_

(1016 entries)

Binder Index

_

other

(47313 entries)

Module Index

J

X

Y

_

other

(784 entries)

Variable Index

J

Q

V

X

Y

_

other

(1547 entries)

Library Index

K

X

Y

_

other

(583 entries)

Lemma Index

other

(11764 entries)

Constructor Index

K

Y

_

other

(959 entries)

Axiom Index

J

K

V

X

Y

_

other

(627 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

V

X

Y

_

other

(475 entries)

Section Index

J

Q

X

Y

_

other

(492 entries)

Instance Index

J

V

X

Y

_

other

(903 entries)

Abbreviation Index

J

Y

_

other

(1448 entries)

Definition Index

_

other

(4360 entries)

Record Index

J

V

X

Y

_

other

(166 entries)

P (abbreviation)

pairT [in Coq.Init.Datatypes]
Pbit [in Coq.NArith.Ndigits]
Pcase [in Coq.PArith.BinPos]
Pcompare [in Coq.PArith.BinPos]
Pcompare_1 [in Coq.PArith.BinPos]
Pcompare_p_Sp [in Coq.PArith.BinPos]
Pcompare_antisym [in Coq.PArith.BinPos]
Pcompare_Lt_Gt [in Coq.PArith.BinPos]
Pcompare_eq_Lt [in Coq.PArith.BinPos]
Pcompare_Gt_Lt [in Coq.PArith.BinPos]
Pcompare_eq_iff [in Coq.PArith.BinPos]
Pcompare_refl_id [in Coq.PArith.BinPos]
Pcompare_nat_compare [in Coq.PArith.Pnat]
Pdouble_minus_one_o_succ_eq_xI [in Coq.PArith.BinPos]
Pdouble_minus_two [in Coq.PArith.BinPos]
Pdouble_plus_one_mask [in Coq.PArith.BinPos]
Pdouble_minus_one [in Coq.PArith.BinPos]
PeanoOne [in Coq.PArith.BinPos]
PeanoSucc [in Coq.PArith.BinPos]
peanoView [in Coq.PArith.BinPos]
PeanoView [in Coq.PArith.BinPos]
PeanoViewUnique [in Coq.PArith.BinPos]
PeanoView_iter [in Coq.PArith.BinPos]
peanoView_xI [in Coq.PArith.BinPos]
peanoView_xO [in Coq.PArith.BinPos]
PeanoView_rec [in Coq.PArith.BinPos]
PeanoView_ind [in Coq.PArith.BinPos]
PeanoView_rect [in Coq.PArith.BinPos]
Peqb_correct [in Coq.NArith.Ndec]
permutation [in Coq.Sorting.PermutEq]
Permutation_app_swap [in Coq.Sorting.Permutation]
permut_tran [in Coq.Sorting.PermutSetoid]
permut_right [in Coq.Sorting.PermutSetoid]
PExpr [in Coq.micromega.EnvRing]
Pge_ge [in Coq.PArith.Pnat]
Pgt_gt [in Coq.PArith.Pnat]
ph [in Coq.ssr.ssrbool]
ph [in Coq.ssr.ssrbool]
phi_pos1 [in Coq.micromega.ZCoeff]
phi_pos [in Coq.micromega.ZCoeff]
Pind [in Coq.PArith.BinPos]
Ple_le [in Coq.PArith.Pnat]
Plt_not_plus_l [in Coq.PArith.BinPos]
Plt_plus_r [in Coq.PArith.BinPos]
Plt_1 [in Coq.PArith.BinPos]
Plt_lt [in Coq.PArith.Pnat]
plus [in Coq.Init.Peano]
plus_minus [in Coq.Arith.Minus]
plus_succ_r_reverse [in Coq.Init.Peano]
plus_0_r_reverse [in Coq.Init.Peano]
plus_tail_plus [in Coq.Arith.Plus]
plus_permute_2_in_4 [in Coq.Arith.Plus]
plus_is_one [in Coq.Arith.Plus]
plus_is_O [in Coq.Arith.Plus]
plus_lt_compat [in Coq.Arith.Plus]
plus_lt_le_compat [in Coq.Arith.Plus]
plus_le_lt_compat [in Coq.Arith.Plus]
plus_le_compat [in Coq.Arith.Plus]
plus_lt_compat_r [in Coq.Arith.Plus]
plus_lt_compat_l [in Coq.Arith.Plus]
plus_le_compat_r [in Coq.Arith.Plus]
plus_le_compat_l [in Coq.Arith.Plus]
plus_lt_reg_l [in Coq.Arith.Plus]
plus_le_reg_l [in Coq.Arith.Plus]
plus_reg_l [in Coq.Arith.Plus]
plus_assoc_reverse [in Coq.Arith.Plus]
plus_Snm_nSm [in Coq.Arith.Plus]
plus_permute [in Coq.Arith.Plus]
plus_assoc [in Coq.Arith.Plus]
plus_comm [in Coq.Arith.Plus]
plus_0_r [in Coq.Arith.Plus]
plus_0_l [in Coq.Arith.Plus]
plus_min_distr_r [in Coq.Arith.Min]
plus_min_distr_l [in Coq.Arith.Min]
plus_lt_is_lt [in Coq.Reals.RIneq]
plus_le_is_le [in Coq.Reals.RIneq]
plus_gt_compat_l [in Coq.Arith.Gt]
plus_gt_reg_l [in Coq.Arith.Gt]
plus_max_distr_r [in Coq.Arith.Max]
plus_max_distr_l [in Coq.Arith.Max]
Pminus [in Coq.PArith.BinPos]
Pminus_Eq [in Coq.PArith.BinPos]
Pminus_Lt [in Coq.PArith.BinPos]
Pminus_mask_Lt [in Coq.PArith.BinPos]
Pminus_minus_distr [in Coq.PArith.BinPos]
Pminus_plus_distr [in Coq.PArith.BinPos]
Pminus_xI_xI [in Coq.PArith.BinPos]
Pminus_decr [in Coq.PArith.BinPos]
Pminus_lt_mono_r [in Coq.PArith.BinPos]
Pminus_compare_mono_r [in Coq.PArith.BinPos]
Pminus_compare_mono_l [in Coq.PArith.BinPos]
Pminus_lt_mono_l [in Coq.PArith.BinPos]
Pminus_mask_diag [in Coq.PArith.BinPos]
Pminus_succ_r [in Coq.PArith.BinPos]
Pminus_mask_carry_spec [in Coq.PArith.BinPos]
Pminus_mask_succ_r [in Coq.PArith.BinPos]
Pminus_mask_carry [in Coq.PArith.BinPos]
Pminus_mask [in Coq.PArith.BinPos]
Pminus_minus [in Coq.PArith.Pnat]
Pmult [in Coq.PArith.BinPos]
Pmult_minus_distr_l [in Coq.PArith.BinPos]
Pmult_le_mono [in Coq.PArith.BinPos]
Pmult_le_mono_r [in Coq.PArith.BinPos]
Pmult_le_mono_l [in Coq.PArith.BinPos]
Pmult_lt_mono [in Coq.PArith.BinPos]
Pmult_lt_mono_r [in Coq.PArith.BinPos]
Pmult_lt_mono_l [in Coq.PArith.BinPos]
Pmult_compare_mono_r [in Coq.PArith.BinPos]
Pmult_compare_mono_l [in Coq.PArith.BinPos]
Pmult_1_inversion_l [in Coq.PArith.BinPos]
Pmult_reg_l [in Coq.PArith.BinPos]
Pmult_reg_r [in Coq.PArith.BinPos]
Pmult_xO_discr [in Coq.PArith.BinPos]
Pmult_xI_mult_xO_discr [in Coq.PArith.BinPos]
Pmult_assoc [in Coq.PArith.BinPos]
Pmult_plus_distr_r [in Coq.PArith.BinPos]
Pmult_plus_distr_l [in Coq.PArith.BinPos]
Pmult_comm [in Coq.PArith.BinPos]
Pmult_xI_permute_r [in Coq.PArith.BinPos]
Pmult_xO_permute_r [in Coq.PArith.BinPos]
Pmult_Sn_m [in Coq.PArith.BinPos]
Pmult_1_r [in Coq.PArith.BinPos]
Pmult_nat [in Coq.PArith.BinPos]
Pmult_mult [in Coq.PArith.Pnat]
Pol [in Coq.micromega.EnvRing]
Poption [in Coq.rtauto.Bintree]
positive [in Coq.PArith.BinPos]
PositiveSet.InL [in Coq.FSets.FSetPositive]
PositiveSet.InL [in Coq.MSets.MSetPositive]
PositiveSet.lex [in Coq.FSets.FSetPositive]
PositiveSet.lex [in Coq.MSets.MSetPositive]
positive_eq_dec [in Coq.PArith.BinPos]
positive_mask_rec [in Coq.PArith.BinPos]
positive_mask_ind [in Coq.PArith.BinPos]
positive_mask_rect [in Coq.PArith.BinPos]
positive_mask [in Coq.PArith.BinPos]
positive_ind [in Coq.PArith.BinPos]
positive_rec [in Coq.PArith.BinPos]
positive_rect [in Coq.PArith.BinPos]
pos_mod_int [in Coq.Numbers.Cyclic.Int63.Cyclic63]
Pos.mul_eq_1 [in Coq.PArith.BinPos]
Pos.sixteen [in Coq.PArith.BinPosDef]
Pos.ten [in Coq.PArith.BinPosDef]
pow [in Coq.Numbers.Natural.Peano.NPeano]
Power [in Coq.Wellfounded.Lexicographic_Exponentiation]
powerRZ_mult_distr [in Coq.Reals.Rfunctions]
powerRZ_neg [in Coq.Reals.Rfunctions]
powerRZ_inv [in Coq.Reals.Rfunctions]
pow_succ_r [in Coq.Numbers.Natural.Peano.NPeano]
pow_0_r [in Coq.Numbers.Natural.Peano.NPeano]
Pplus [in Coq.PArith.BinPos]
Pplus_minus_assoc [in Coq.PArith.BinPos]
Pplus_minus_eq [in Coq.PArith.BinPos]
Pplus_le_mono [in Coq.PArith.BinPos]
Pplus_le_mono_r [in Coq.PArith.BinPos]
Pplus_le_mono_l [in Coq.PArith.BinPos]
Pplus_lt_mono [in Coq.PArith.BinPos]
Pplus_lt_mono_r [in Coq.PArith.BinPos]
Pplus_lt_mono_l [in Coq.PArith.BinPos]
Pplus_compare_mono_r [in Coq.PArith.BinPos]
Pplus_compare_mono_l [in Coq.PArith.BinPos]
Pplus_diag [in Coq.PArith.BinPos]
Pplus_xO_double_minus_one [in Coq.PArith.BinPos]
Pplus_xI_double_minus_one [in Coq.PArith.BinPos]
Pplus_xO [in Coq.PArith.BinPos]
Pplus_assoc [in Coq.PArith.BinPos]
Pplus_carry_reg_l [in Coq.PArith.BinPos]
Pplus_carry_reg_r [in Coq.PArith.BinPos]
Pplus_reg_l [in Coq.PArith.BinPos]
Pplus_reg_r [in Coq.PArith.BinPos]
Pplus_carry_plus [in Coq.PArith.BinPos]
Pplus_no_neutral [in Coq.PArith.BinPos]
Pplus_succ_permute_l [in Coq.PArith.BinPos]
Pplus_succ_permute_r [in Coq.PArith.BinPos]
Pplus_comm [in Coq.PArith.BinPos]
Pplus_carry_spec [in Coq.PArith.BinPos]
Pplus_carry [in Coq.PArith.BinPos]
Pplus_plus [in Coq.PArith.Pnat]
Ppred_Nsucc [in Coq.NArith.BinNat]
Ppred_N_spec [in Coq.NArith.BinNat]
Prec [in Coq.PArith.BinPos]
Prect [in Coq.PArith.BinPos]
Prect_base [in Coq.PArith.BinPos]
Prect_succ [in Coq.PArith.BinPos]
pred [in Coq.Init.Peano]
predicate [in Coq.Classes.RelationClasses]
PredicateExtensionality [in Coq.Logic.PropExtensionalityFacts]
pred_of_minus [in Coq.Arith.Minus]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [in Coq.PArith.Pnat]
pred_of_simpl [in Coq.ssr.ssrbool]
prodT [in Coq.Init.Datatypes]
prodT_curry [in Coq.Init.Datatypes]
prodT_uncurry [in Coq.Init.Datatypes]
prodT_ind [in Coq.Init.Datatypes]
prodT_rec [in Coq.Init.Datatypes]
prodT_rect [in Coq.Init.Datatypes]
prod_f_SO [in Coq.Reals.Rprod]
prod_curry [in Coq.Init.Datatypes]
prod_uncurry [in Coq.Init.Datatypes]
prod_curry_uncurry [in Coq.Program.Combinators]
prod_uncurry_curry [in Coq.Program.Combinators]
prod_neq_R0 [in Coq.Reals.RIneq]
PropositionalExtensionality [in Coq.Logic.PropExtensionalityFacts]
PropositionalFunctionalExtensionality [in Coq.Logic.PropExtensionalityFacts]
ProvablePropositionExtensionality [in Coq.Logic.PropExtensionalityFacts]
Psize [in Coq.PArith.BinPos]
Psize_pos_le [in Coq.PArith.BinPos]
Psize_pos_gt [in Coq.PArith.BinPos]
Psize_monotone [in Coq.PArith.BinPos]
Psize_pos [in Coq.PArith.BinPos]
Psquare_correct [in Coq.ZArith.Zpow_facts]
Psucc_pred [in Coq.PArith.BinPos]
Psucc_not_one [in Coq.PArith.BinPos]
Psucc_o_double_minus_one_eq_xO [in Coq.PArith.BinPos]
Psucc_S [in Coq.PArith.Pnat]
push [in Coq.micromega.Tauto]
Pxor [in Coq.NArith.Ndigits]
P_of_succ_nat [in Coq.PArith.BinPos]
P_of_succ_nat_o_nat_of_P_eq_succ [in Coq.PArith.Pnat]
P_of_succ_nat_of_P [in Coq.PArith.Pnat]
P_Rmin [in Coq.Reals.Rpower]

Global Index

(72745 entries)

Notation Index

F

J

K

T

X

Y

_

(1016 entries)

Binder Index

_

other

(47313 entries)

Module Index

J

X

Y

_

other

(784 entries)

Variable Index

J

Q

V

X

Y

_

other

(1547 entries)

Library Index

K

X

Y

_

other

(583 entries)

Lemma Index

other

(11764 entries)

Constructor Index

K

Y

_

other

(959 entries)

Axiom Index

J

K

V

X

Y

_

other

(627 entries)

Inductive Index

X

Y

_

other

(308 entries)

Projection Index

G

K

V

X

Y

_

other

(475 entries)

Section Index

J

Q

X

Y

_

other

(492 entries)

Instance Index

J

V

X

Y

_

other

(903 entries)

Abbreviation Index

J

Y

_

other

(1448 entries)

Definition Index

_

other

(4360 entries)

Record Index

J

V

X

Y

_

other

(166 entries)