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 (21445 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 (889 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 (714 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 (1464 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 (482 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 (10031 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 (663 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 (537 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 (374 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 (285 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 (457 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 (616 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 (1328 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 (3468 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 (137 entries)

Z (definition)

Zabs_dec [in Coq.ZArith.Zabs]
ZBitsProp.b2z [in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit [in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.eqf [in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot [in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones [in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit [in Coq.Numbers.Integer.Abstract.ZBits]
ZChecker [in Coq.micromega.ZMicromega]
Zdeduce [in Coq.micromega.ZMicromega]
zdigits [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zdivide_intro [in Coq.ZArith.Znumtheory]
Zdiv_rest [in Coq.ZArith.Zpower]
Zdiv_rest_aux [in Coq.ZArith.Zpower]
Zdiv_pol [in Coq.micromega.ZMicromega]
Zeq_bool [in Coq.ZArith.Zbool]
zero [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
zero [in Coq.Init.Nat]
zero [in Coq.Strings.Ascii]
zerob [in Coq.Bool.Zerob]
zerop [in Coq.Arith.Compare_dec]
zerop_bool [in Coq.Arith.Bool_nat]
ZEuclid.div [in Coq.ZArith.Zeuclid]
ZEuclid.modulo [in Coq.ZArith.Zeuclid]
Zeval_op1 [in Coq.micromega.ZMicromega]
Zeval_formula' [in Coq.micromega.ZMicromega]
Zeval_formula [in Coq.micromega.ZMicromega]
Zeval_op2 [in Coq.micromega.ZMicromega]
Zeval_expr [in Coq.micromega.ZMicromega]
Zeven [in Coq.ZArith.Zeven]
Zeven_odd_bool [in Coq.ZArith.Zbool]
Zeven_dec [in Coq.ZArith.Zeven]
Zeven_odd_dec [in Coq.ZArith.Zeven]
ZgcdM [in Coq.micromega.ZMicromega]
Zgcdn [in Coq.ZArith.Zgcd_alt]
ZGcdProp.Bezout [in Coq.Numbers.Integer.Abstract.ZGcd]
Zgcd_alt [in Coq.ZArith.Zgcd_alt]
Zgcd_bound [in Coq.ZArith.Zgcd_alt]
Zgcd_pol [in Coq.micromega.ZMicromega]
zipWith [in Coq.Lists.Streams]
ZLcmProp.lcm [in Coq.Numbers.Integer.Abstract.ZLcm]
Zlength [in Coq.ZArith.Zcomplements]
Zlength_aux [in Coq.ZArith.Zcomplements]
Zle_bool_total [in Coq.ZArith.Zbool]
ZModuloCyclicType.t [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zmod_POS [in Coq.ZArith.Zdiv]
Zmod' [in Coq.ZArith.Zdiv]
Zmod2 [in Coq.ZArith.Zdigits]
zmon_pred [in Coq.micromega.EnvRing]
zmon_pred [in Coq.setoid_ring.Ring_polynom]
ZMulOrderProp.mul_eq_1 [in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZN [in Coq.setoid_ring.Ncring]
Zne [in Coq.ZArith.BinInt]
Zneg' [in Coq.omega.PreOmega]
Zneq_bool [in Coq.ZArith.Zbool]
ZnZ.of_Z [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.OW [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.OW' [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WO [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WO' [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW' [in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zn2z_to_Z [in Coq.Numbers.Cyclic.Abstract.DoubleType]
Zodd [in Coq.ZArith.Zeven]
Zodd_dec [in Coq.ZArith.Zeven]
ZPairsAxiomsMod.add [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.eq [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.le [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.one [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.pred [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.succ [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.t [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.two [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.zero [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.add [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.eq [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.le [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.lt [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.max [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.min [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.mul [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.one [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.opp [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.pred [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.sub [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.succ [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.t [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.two [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.zero [in Coq.Numbers.Integer.NatPairs.ZNatPairs]
Zpos' [in Coq.omega.PreOmega]
Zpower_nat [in Coq.ZArith.Zpower]
Zpower_alt [in Coq.ZArith.Zpow_alt]
Zpow_mod [in Coq.ZArith.Zpow_facts]
Zpow_mod_pos [in Coq.ZArith.Zpow_facts]
ZQuotProp.Private_Div.Quot2Div.mod_bound_pos [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.div_mod [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.mod_wd [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.div_wd [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.modulo [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.div [in Coq.Numbers.Integer.Abstract.ZDivTrunc]
Zsqrt [in Coq.ZArith.Zsqrt_compat]
Zsqrt_plain [in Coq.ZArith.Zsqrt_compat]
ZTautoChecker [in Coq.micromega.ZMicromega]
ZtoN [in Coq.setoid_ring.Field_theory]
Zunsat [in Coq.micromega.ZMicromega]
ZWeakChecker [in Coq.micromega.ZMicromega]
ZweakTautoChecker [in Coq.micromega.ZMicromega]
Zwf [in Coq.ZArith.Zwf]
Zwf_up [in Coq.ZArith.Zwf]
ZWitness [in Coq.micromega.ZMicromega]
Z_of_N' [in Coq.omega.PreOmega]
Z_of_nat' [in Coq.omega.PreOmega]
Z_noteq_bool [in Coq.ZArith.Zbool]
Z_eq_bool [in Coq.ZArith.Zbool]
Z_gt_le_bool [in Coq.ZArith.Zbool]
Z_le_gt_bool [in Coq.ZArith.Zbool]
Z_ge_lt_bool [in Coq.ZArith.Zbool]
Z_lt_ge_bool [in Coq.ZArith.Zbool]
Z_le_lt_eq_dec [in Coq.ZArith.ZArith_dec]
Z_ge_lt_dec [in Coq.ZArith.ZArith_dec]
Z_gt_le_dec [in Coq.ZArith.ZArith_dec]
Z_le_gt_dec [in Coq.ZArith.ZArith_dec]
Z_lt_ge_dec [in Coq.ZArith.ZArith_dec]
Z_ge_dec [in Coq.ZArith.ZArith_dec]
Z_gt_dec [in Coq.ZArith.ZArith_dec]
Z_le_dec [in Coq.ZArith.ZArith_dec]
Z_lt_dec [in Coq.ZArith.ZArith_dec]
z_of_int [in Coq.extraction.ExtrOcamlIntConv]
Z_as_OT.eq_dec [in Coq.Structures.OrderedTypeEx]
Z_as_OT.compare [in Coq.Structures.OrderedTypeEx]
Z_as_OT.lt [in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq_trans [in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq_sym [in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq_refl [in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq [in Coq.Structures.OrderedTypeEx]
Z_as_OT.t [in Coq.Structures.OrderedTypeEx]
Z_as_Int.diveucl_spec [in Coq.romega.ReflOmegaCore]
Z_as_Int.diveucl [in Coq.romega.ReflOmegaCore]
Z_as_Int.le_lt_int [in Coq.romega.ReflOmegaCore]
Z_as_Int.compare_Eq [in Coq.romega.ReflOmegaCore]
Z_as_Int.compare [in Coq.romega.ReflOmegaCore]
Z_as_Int.mult_lt_compat_l [in Coq.romega.ReflOmegaCore]
Z_as_Int.plus_le_compat [in Coq.romega.ReflOmegaCore]
Z_as_Int.lt_0_1 [in Coq.romega.ReflOmegaCore]
Z_as_Int.lt_not_eq [in Coq.romega.ReflOmegaCore]
Z_as_Int.lt_trans [in Coq.romega.ReflOmegaCore]
Z_as_Int.gt_lt_iff [in Coq.romega.ReflOmegaCore]
Z_as_Int.ge_le_iff [in Coq.romega.ReflOmegaCore]
Z_as_Int.le_lt_iff [in Coq.romega.ReflOmegaCore]
Z_as_Int.gt [in Coq.romega.ReflOmegaCore]
Z_as_Int.ge [in Coq.romega.ReflOmegaCore]
Z_as_Int.lt [in Coq.romega.ReflOmegaCore]
Z_as_Int.le [in Coq.romega.ReflOmegaCore]
Z_as_Int.mult [in Coq.romega.ReflOmegaCore]
Z_as_Int.minus [in Coq.romega.ReflOmegaCore]
Z_as_Int.opp [in Coq.romega.ReflOmegaCore]
Z_as_Int.plus [in Coq.romega.ReflOmegaCore]
Z_as_Int.one [in Coq.romega.ReflOmegaCore]
Z_as_Int.zero [in Coq.romega.ReflOmegaCore]
Z_as_Int.t [in Coq.romega.ReflOmegaCore]
Z_as_Int.i2z [in Coq.ZArith.Int]
Z_as_Int.ge_lt_dec [in Coq.ZArith.Int]
Z_as_Int.gt_le_dec [in Coq.ZArith.Int]
Z_as_Int.eq_dec [in Coq.ZArith.Int]
Z_as_Int.leb [in Coq.ZArith.Int]
Z_as_Int.ltb [in Coq.ZArith.Int]
Z_as_Int.eqb [in Coq.ZArith.Int]
Z_as_Int.max [in Coq.ZArith.Int]
Z_as_Int.mul [in Coq.ZArith.Int]
Z_as_Int.sub [in Coq.ZArith.Int]
Z_as_Int.opp [in Coq.ZArith.Int]
Z_as_Int.add [in Coq.ZArith.Int]
Z_as_Int._3 [in Coq.ZArith.Int]
Z_as_Int._2 [in Coq.ZArith.Int]
Z_as_Int._1 [in Coq.ZArith.Int]
Z_as_Int._0 [in Coq.ZArith.Int]
Z_as_Int.t [in Coq.ZArith.Int]
z_of_bigint [in Coq.extraction.ExtrOcamlBigIntConv]
Z.abs [in Coq.ZArith.BinIntDef]
Z.abs_N [in Coq.ZArith.BinIntDef]
Z.abs_nat [in Coq.ZArith.BinIntDef]
Z.add [in Coq.ZArith.BinIntDef]
Z.add_wd [in Coq.ZArith.BinInt]
Z.compare [in Coq.ZArith.BinIntDef]
Z.div [in Coq.ZArith.BinIntDef]
Z.divide [in Coq.ZArith.BinInt]
Z.div_eucl [in Coq.ZArith.BinIntDef]
Z.div_wd [in Coq.ZArith.BinInt]
Z.div2 [in Coq.ZArith.BinIntDef]
Z.double [in Coq.ZArith.BinIntDef]
Z.eq [in Coq.ZArith.BinInt]
Z.eqb [in Coq.ZArith.BinIntDef]
Z.eq_dec [in Coq.ZArith.BinInt]
Z.eq_equiv [in Coq.ZArith.BinInt]
Z.even [in Coq.ZArith.BinIntDef]
Z.Even [in Coq.ZArith.BinInt]
Z.gcd [in Coq.ZArith.BinIntDef]
Z.ge [in Coq.ZArith.BinInt]
Z.geb [in Coq.ZArith.BinIntDef]
Z.ggcd [in Coq.ZArith.BinIntDef]
Z.gt [in Coq.ZArith.BinInt]
Z.gtb [in Coq.ZArith.BinIntDef]
Z.iter [in Coq.ZArith.BinIntDef]
Z.land [in Coq.ZArith.BinIntDef]
Z.ldiff [in Coq.ZArith.BinIntDef]
Z.le [in Coq.ZArith.BinInt]
Z.leb [in Coq.ZArith.BinIntDef]
Z.log2 [in Coq.ZArith.BinIntDef]
Z.lor [in Coq.ZArith.BinIntDef]
Z.lt [in Coq.ZArith.BinInt]
Z.ltb [in Coq.ZArith.BinIntDef]
Z.lt_wd [in Coq.ZArith.BinInt]
Z.lxor [in Coq.ZArith.BinIntDef]
Z.max [in Coq.ZArith.BinIntDef]
Z.min [in Coq.ZArith.BinIntDef]
Z.modulo [in Coq.ZArith.BinIntDef]
Z.mod_bound_pos [in Coq.ZArith.BinInt]
Z.mod_wd [in Coq.ZArith.BinInt]
Z.mul [in Coq.ZArith.BinIntDef]
Z.mul_wd [in Coq.ZArith.BinInt]
Z.odd [in Coq.ZArith.BinIntDef]
Z.Odd [in Coq.ZArith.BinInt]
Z.of_N [in Coq.ZArith.BinIntDef]
Z.of_nat [in Coq.ZArith.BinIntDef]
Z.one [in Coq.ZArith.BinIntDef]
Z.opp [in Coq.ZArith.BinIntDef]
Z.opp_wd [in Coq.ZArith.BinInt]
Z.pos_div_eucl [in Coq.ZArith.BinIntDef]
Z.pos_sub [in Coq.ZArith.BinIntDef]
Z.pow [in Coq.ZArith.BinIntDef]
Z.pow_pos [in Coq.ZArith.BinIntDef]
Z.pow_wd [in Coq.ZArith.BinInt]
Z.pred [in Coq.ZArith.BinIntDef]
Z.pred_double [in Coq.ZArith.BinIntDef]
Z.pred_wd [in Coq.ZArith.BinInt]
Z.quot [in Coq.ZArith.BinIntDef]
Z.quotrem [in Coq.ZArith.BinIntDef]
Z.quot_wd [in Coq.ZArith.BinInt]
Z.quot2 [in Coq.ZArith.BinIntDef]
Z.rem [in Coq.ZArith.BinIntDef]
Z.rem_wd [in Coq.ZArith.BinInt]
Z.sgn [in Coq.ZArith.BinIntDef]
Z.shiftl [in Coq.ZArith.BinIntDef]
Z.shiftr [in Coq.ZArith.BinIntDef]
Z.sqrt [in Coq.ZArith.BinIntDef]
Z.sqrtrem [in Coq.ZArith.BinIntDef]
Z.square [in Coq.ZArith.BinIntDef]
Z.sub [in Coq.ZArith.BinIntDef]
Z.sub_wd [in Coq.ZArith.BinInt]
Z.succ [in Coq.ZArith.BinIntDef]
Z.succ_double [in Coq.ZArith.BinIntDef]
Z.succ_wd [in Coq.ZArith.BinInt]
Z.t [in Coq.ZArith.BinIntDef]
Z.testbit [in Coq.ZArith.BinIntDef]
Z.testbit_wd [in Coq.ZArith.BinInt]
Z.to_pos [in Coq.ZArith.BinIntDef]
Z.to_N [in Coq.ZArith.BinIntDef]
Z.to_nat [in Coq.ZArith.BinIntDef]
Z.two [in Coq.ZArith.BinIntDef]
Z.zero [in Coq.ZArith.BinIntDef]



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 (21445 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 (889 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 (714 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 (1464 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 (482 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 (10031 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 (663 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 (537 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 (374 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 (285 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 (457 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 (616 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 (1328 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 (3468 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 (137 entries)