P (definition)
ParamDefiniteDescription [in Coq.Logic.ChoiceFacts]
Pcompare [in Coq.NArith.BinPos]
Pcompare [in Coq.Arith.Compare]
Pdiv2 [in Coq.NArith.BinPos]
Pdouble_mask [in Coq.NArith.BinPos]
Pdouble_minus_one [in Coq.NArith.BinPos]
Pdouble_minus_two [in Coq.NArith.BinPos]
Pdouble_plus_one_mask [in Coq.NArith.BinPos]
permutation [in Coq.Sorting.Permutation]
phi_sequence [in Coq.Reals.RiemannInt]
PI [in Coq.Reals.AltSeries]
PI_tg [in Coq.Reals.AltSeries]
plat [in Coq.Reals.Rtrigo_calc]
plus [in Coq.Init.Peano]
plus_acc [in Coq.Arith.Plus]
plus_fct [in Coq.Reals.Ranalysis1]
plus_is_one [in Coq.Arith.Plus]
plus_iter [in Coq.NArith.BinPos]
Pminus [in Coq.NArith.BinPos]
Pminus_mask [in Coq.NArith.BinPos]
Pminus_mask_carry [in Coq.NArith.BinPos]
Pmult [in Coq.NArith.BinPos]
Pmult_nat [in Coq.NArith.BinPos]
point_adherent [in Coq.Reals.Rtopology]
positivity_seq [in Coq.Reals.AltSeries]
pos_Rl [in Coq.Reals.RList]
Pow [in Coq.Relations.Relation_Operators]
pow [in Coq.Logic.Berardi]
pow [in Coq.Reals.Rfunctions]
powerRZ [in Coq.Reals.Rfunctions]
Power_set_PO [in Coq.Sets.Powerset]
pow_fct [in Coq.Reals.Ranalysis1]
pow_2_n [in Coq.Reals.Rsqrt_def]
Pplus [in Coq.NArith.BinPos]
Pplus_carry [in Coq.NArith.BinPos]
Ppred [in Coq.NArith.BinPos]
Prec [in Coq.NArith.BinPos]
pred [in Coq.Init.Peano]
PredicateExtensionality [in Coq.Logic.Diaconescu]
primitive [in Coq.Reals.RiemannInt]
prodT_curry [in Coq.Init.Logic_Type]
prodT_uncurry [in Coq.Init.Logic_Type]
prod_f_SO [in Coq.Reals.Rprod]
projS1 [in Coq.Init.Specif]
projS2 [in Coq.Init.Specif]
projT1 [in Coq.Init.Specif]
projT2 [in Coq.Init.Specif]
proj1_sig [in Coq.Init.Specif]
proj2_sig [in Coq.Init.Specif]
ProofIrrelevance [in Coq.Logic.ChoiceFacts]
proof_irrelevance [in Coq.Logic.ClassicalFacts]
prop_degeneracy [in Coq.Logic.ClassicalFacts]
prop_extensionality [in Coq.Logic.ClassicalFacts]
Prop_S [in Coq.Setoids.Setoid]
Pser [in Coq.Reals.Rseries]
Psucc [in Coq.NArith.BinPos]
p2b [in Coq.Logic.ProofIrrelevance]
P_of_succ_nat [in Coq.NArith.BinPos]
p_xor [in Coq.IntMap.Addr]
This page has been generated by coqdoc