| 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) |
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_lt_is_lt [in Coq.Reals.RIneq]
plus_le_is_le [in Coq.Reals.RIneq]
plus_permute_2_in_4 [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_succ_r_reverse [in Coq.Init.Peano]
plus_0_r_reverse [in Coq.Init.Peano]
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.ten [in Coq.PArith.BinPosDef]
pow [in Coq.Numbers.Natural.Peano.NPeano]
Power [in Coq.Wellfounded.Lexicographic_Exponentiation]
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_simpl [in Coq.ssr.ssrbool]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [in Coq.PArith.Pnat]
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_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]
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]
| 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) |