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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)

P (definition)

PairDecidableType.eq [in eq]
PairDecidableType.eq [in eq]
PairDecidableType.eq_dec [in eq_dec]
PairDecidableType.eq_dec [in eq_dec]
PairDecidableType.t [in t]
PairDecidableType.t [in t]
PairOrderedType.compare [in compare]
PairOrderedType.compare [in compare]
PairOrderedType.eq [in eq]
PairOrderedType.eq_dec [in eq_dec]
PairOrderedType.lt [in lt]
PairOrderedType.lt [in lt]
PairOrderedType.t [in t]
PairUsualDecidableType.eq [in eq]
PairUsualDecidableType.eq [in eq]
PairUsualDecidableType.eq_refl [in eq_refl]
PairUsualDecidableType.eq_sym [in eq_sym]
PairUsualDecidableType.eq_trans [in eq_trans]
PairUsualDecidableType.eq_dec [in eq_dec]
PairUsualDecidableType.eq_dec [in eq_dec]
PairUsualDecidableType.t [in t]
PairUsualDecidableType.t [in t]
partition [in partition]
Pcompare [in Pcompare]
Pdiv [in Pdiv]
Pdiv_eucl [in Pdiv_eucl]
Pdiv_eucl_correct [in Pdiv_eucl_correct]
pequiv [in pequiv]
permutation [in permutation]
phi [in phi]
phibis_aux [in phibis_aux]
phi_inv_positive [in phi_inv_positive]
phi_inv2 [in phi_inv2]
phi_sequence [in phi_sequence]
phi_inv [in phi_inv]
phi2 [in phi2]
PI [in PI]
PI_tg [in PI_tg]
PI_2_3_7_tg [in PI_2_3_7_tg]
PI_2_aux [in PI_2_aux]
PI.proof_irrelevance [in proof_irrelevance]
PI2 [in PI2]
plat [in plat]
plength [in plength]
plus [in plus]
plusnS [in plusnS]
plusn0 [in plusn0]
plus_0_r [in plus_0_r]
plus_max_distr_l [in plus_max_distr_l]
plus_max_distr_r [in plus_max_distr_r]
plus_Snm_nSm [in plus_Snm_nSm]
plus_is_one [in plus_is_one]
plus_min_distr_l [in plus_min_distr_l]
plus_fct [in plus_fct]
plus_min_distr_r [in plus_min_distr_r]
pointwise_relation [in pointwise_relation]
pointwise_lifting [in pointwise_lifting]
pointwise_extension [in pointwise_extension]
point_adherent [in point_adherent]
PositiveMap.add [in add]
PositiveMap.cardinal [in cardinal]
PositiveMap.elements [in elements]
PositiveMap.empty [in empty]
PositiveMap.Empty [in Empty]
PositiveMap.equal [in equal]
PositiveMap.Equal [in Equal]
PositiveMap.Equiv [in Equiv]
PositiveMap.Equivb [in Equivb]
PositiveMap.eq_key_elt [in eq_key_elt]
PositiveMap.eq_key [in eq_key]
PositiveMap.find [in find]
PositiveMap.fold [in fold]
PositiveMap.In [in In]
PositiveMap.is_empty [in is_empty]
PositiveMap.key [in key]
PositiveMap.lt_key [in lt_key]
PositiveMap.map [in map]
PositiveMap.mapi [in mapi]
PositiveMap.MapsTo [in MapsTo]
PositiveMap.map2 [in map2]
PositiveMap.mem [in mem]
PositiveMap.remove [in remove]
PositiveMap.t [in t]
PositiveMap.tree_ind [in tree_ind]
PositiveMap.xelements [in xelements]
PositiveMap.xfind [in xfind]
PositiveMap.xfoldi [in xfoldi]
PositiveMap.xmapi [in xmapi]
PositiveMap.xmap2_l [in xmap2_l]
PositiveMap.xmap2_r [in xmap2_r]
PositiveMap._map2 [in _map2]
PositiveOrderedTypeBits.bits_lt [in bits_lt]
PositiveOrderedTypeBits.bits_lt [in bits_lt]
PositiveOrderedTypeBits.compare [in compare]
PositiveOrderedTypeBits.compare [in compare]
PositiveOrderedTypeBits.eq [in eq]
PositiveOrderedTypeBits.eqb [in eqb]
PositiveOrderedTypeBits.eqb_eq [in eqb_eq]
PositiveOrderedTypeBits.eq_refl [in eq_refl]
PositiveOrderedTypeBits.eq_sym [in eq_sym]
PositiveOrderedTypeBits.eq_trans [in eq_trans]
PositiveOrderedTypeBits.lt [in lt]
PositiveOrderedTypeBits.lt [in lt]
PositiveOrderedTypeBits.t [in t]
PositiveOrderedTypeBits.t [in t]
PositiveSet.add [in add]
PositiveSet.add [in add]
PositiveSet.cardinal [in cardinal]
PositiveSet.cardinal [in cardinal]
PositiveSet.choose [in choose]
PositiveSet.choose [in choose]
PositiveSet.compare [in compare]
PositiveSet.compare_fun [in compare_fun]
PositiveSet.compare_bool [in compare_bool]
PositiveSet.compare_bool [in compare_bool]
PositiveSet.diff [in diff]
PositiveSet.diff [in diff]
PositiveSet.elements [in elements]
PositiveSet.elements [in elements]
PositiveSet.elt [in elt]
PositiveSet.elt [in elt]
PositiveSet.empty [in empty]
PositiveSet.empty [in empty]
PositiveSet.Empty [in Empty]
PositiveSet.Empty [in Empty]
PositiveSet.eq [in eq]
PositiveSet.eq [in eq]
PositiveSet.equal [in equal]
PositiveSet.equal [in equal]
PositiveSet.Equal [in Equal]
PositiveSet.Equal [in Equal]
PositiveSet.Exists [in Exists]
PositiveSet.Exists [in Exists]
PositiveSet.exists_ [in exists_]
PositiveSet.exists_ [in exists_]
PositiveSet.filter [in filter]
PositiveSet.filter [in filter]
PositiveSet.fold [in fold]
PositiveSet.fold [in fold]
PositiveSet.For_all [in For_all]
PositiveSet.For_all [in For_all]
PositiveSet.for_all [in for_all]
PositiveSet.for_all [in for_all]
PositiveSet.In [in In]
PositiveSet.In [in In]
PositiveSet.inter [in inter]
PositiveSet.inter [in inter]
PositiveSet.is_empty [in is_empty]
PositiveSet.is_empty [in is_empty]
PositiveSet.lt [in lt]
PositiveSet.lt [in lt]
PositiveSet.max_elt [in max_elt]
PositiveSet.max_elt [in max_elt]
PositiveSet.mem [in mem]
PositiveSet.mem [in mem]
PositiveSet.min_elt [in min_elt]
PositiveSet.min_elt [in min_elt]
PositiveSet.node [in node]
PositiveSet.node [in node]
PositiveSet.omap [in omap]
PositiveSet.omap [in omap]
PositiveSet.partition [in partition]
PositiveSet.partition [in partition]
PositiveSet.remove [in remove]
PositiveSet.remove [in remove]
PositiveSet.rev [in rev]
PositiveSet.rev [in rev]
PositiveSet.rev_append [in rev_append]
PositiveSet.rev_append [in rev_append]
PositiveSet.singleton [in singleton]
PositiveSet.singleton [in singleton]
PositiveSet.Subset [in Subset]
PositiveSet.Subset [in Subset]
PositiveSet.subset [in subset]
PositiveSet.subset [in subset]
PositiveSet.t [in t]
PositiveSet.t [in t]
PositiveSet.tree_ind [in tree_ind]
PositiveSet.tree_ind [in tree_ind]
PositiveSet.union [in union]
PositiveSet.union [in union]
PositiveSet.xelements [in xelements]
PositiveSet.xelements [in xelements]
PositiveSet.xexists [in xexists]
PositiveSet.xexists [in xexists]
PositiveSet.xfilter [in xfilter]
PositiveSet.xfilter [in xfilter]
PositiveSet.xfold [in xfold]
PositiveSet.xfold [in xfold]
PositiveSet.xforall [in xforall]
PositiveSet.xforall [in xforall]
PositiveSet.xpartition [in xpartition]
PositiveSet.xpartition [in xpartition]
Positive_as_OT.eq_refl [in eq_refl]
Positive_as_OT.t [in t]
Positive_as_OT.compare [in compare]
Positive_as_OT.eq_sym [in eq_sym]
Positive_as_OT.lt_trans [in lt_trans]
Positive_as_OT.eq_trans [in eq_trans]
Positive_as_OT.eq_dec [in eq_dec]
positive_to_int31 [in positive_to_int31]
Positive_as_OT.lt [in lt]
Positive_as_OT.eq [in eq]
positivity_seq [in positivity_seq]
pos_half_prf [in pos_half_prf]
pos_half [in pos_half]
pos_Rl [in pos_Rl]
pos_mod [in pos_mod]
Pos.add [in add]
Pos.add_carry [in add_carry]
Pos.compare [in compare]
Pos.compare_cont [in compare_cont]
Pos.divide [in divide]
Pos.div2 [in div2]
Pos.div2_up [in div2_up]
Pos.double_mask [in double_mask]
Pos.double_pred_mask [in double_pred_mask]
Pos.eq [in eq]
Pos.eqb [in eqb]
Pos.eq_equiv [in eq_equiv]
Pos.gcd [in gcd]
Pos.gcdn [in gcdn]
Pos.ge [in ge]
Pos.ggcd [in ggcd]
Pos.ggcdn [in ggcdn]
Pos.gt [in gt]
Pos.iter [in iter]
Pos.iter_op [in iter_op]
Pos.land [in land]
Pos.ldiff [in ldiff]
Pos.le [in le]
Pos.leb [in leb]
Pos.le_lteq [in le_lteq]
Pos.lor [in lor]
Pos.lt [in lt]
Pos.ltb [in ltb]
Pos.lxor [in lxor]
Pos.mask2cmp [in mask2cmp]
Pos.max [in max]
Pos.min [in min]
Pos.mul [in mul]
Pos.Ndouble [in Ndouble]
Pos.Nsucc_double [in Nsucc_double]
Pos.of_nat [in of_nat]
Pos.of_succ_nat [in of_succ_nat]
Pos.peanoView [in peanoView]
Pos.PeanoView_iter [in PeanoView_iter]
Pos.peanoView_xI [in peanoView_xI]
Pos.peanoView_xO [in peanoView_xO]
Pos.peano_ind [in peano_ind]
Pos.peano_rec [in peano_rec]
Pos.peano_rect [in peano_rect]
Pos.pow [in pow]
Pos.pred [in pred]
Pos.pred_double [in pred_double]
Pos.pred_N [in pred_N]
Pos.pred_mask [in pred_mask]
Pos.shiftl [in shiftl]
Pos.shiftl_nat [in shiftl_nat]
Pos.shiftr [in shiftr]
Pos.shiftr_nat [in shiftr_nat]
Pos.size [in size]
Pos.size_nat [in size_nat]
Pos.sqrt [in sqrt]
Pos.sqrtrem [in sqrtrem]
Pos.sqrtrem_step [in sqrtrem_step]
Pos.square [in square]
Pos.sub [in sub]
Pos.sub_mask_carry [in sub_mask_carry]
Pos.sub_mask [in sub_mask]
Pos.succ [in succ]
Pos.succ_double_mask [in succ_double_mask]
Pos.switch_Eq [in switch_Eq]
Pos.t [in t]
Pos.testbit [in testbit]
Pos.testbit_nat [in testbit_nat]
Pos.to_nat [in to_nat]
Pos2Z.inj_divide [in inj_divide]
Pow [in Pow]
pow [in pow]
pow [in pow]
pow [in pow]
powerRZ [in powerRZ]
Power_set_PO [in Power_set_PO]
pow_fct [in pow_fct]
pow_2_n [in pow_2_n]
Pplength [in Pplength]
pred [in pred]
pred [in pred]
PredicateExtensionality [in PredicateExtensionality]
predicate_intersection [in predicate_intersection]
predicate_union [in predicate_union]
predicate_all [in predicate_all]
predicate_equivalence [in predicate_equivalence]
predicate_implication [in predicate_implication]
predicate_exists [in predicate_exists]
pred_c [in pred_c]
prefix [in prefix]
pre_atan [in pre_atan]
prime_dec [in prime_dec]
prime_dec_aux [in prime_dec_aux]
prime' [in prime']
primitive [in primitive]
prod_curry [in prod_curry]
prod_f_R0 [in prod_f_R0]
prod_uncurry [in prod_uncurry]
projT1 [in projT1]
projT2 [in projT2]
proj1_inf [in proj1_inf]
proj1_sig [in proj1_sig]
proj2_sig [in proj2_sig]
ProofIrrelevance [in ProofIrrelevance]
ProofIrrelevanceTheory.eq_indd [in eq_indd]
proof_irrelevance [in proof_irrelevance]
proper_inverse_proper [in proper_inverse_proper]
Props.bst_ind [in bst_ind]
Props.Empty [in Empty]
Props.Equal [in Equal]
Props.Exists [in Exists]
Props.For_all [in For_all]
Props.gtb_tree [in gtb_tree]
Props.gt_tree [in gt_tree]
Props.In [in In]
Props.IsOk [in IsOk]
Props.isok [in isok]
Props.ltb_tree [in ltb_tree]
Props.lt_tree [in lt_tree]
Props.Subset [in Subset]
Props.tree_ind [in tree_ind]
prop_degeneracy [in prop_degeneracy]
prop_extensionality [in prop_extensionality]
provable_prop_extensionality [in provable_prop_extensionality]
Pser [in Pser]
ps_atan [in ps_atan]
ps_atan_exists_01 [in ps_atan_exists_01]
ps_atan_exists_1 [in ps_atan_exists_1]
Ptail [in Ptail]
P' [in P']
p2b [in p2b]
P2Bv [in P2Bv]
p2i [in p2i]
p2ibis [in p2ibis]



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 (18816 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 (644 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 (708 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 (1456 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 (407 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 (8932 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 (422 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 (699 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 (209 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 (203 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 (550 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 (338 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 (1235 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 (2946 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 (67 entries)