| 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 | (70451 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 | (1003 entries) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 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]
ZcompareZ [in Coq.micromega.ZifyComparison]
Zdeduce [in Coq.micromega.ZMicromega]
zdigits [in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zdigits2 [in Coq.Floats.SpecFloat]
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.Floats.PrimFloat]
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_bop2 [in Coq.micromega.ZMicromega]
Zeval_pop2 [in Coq.micromega.ZMicromega]
Zeval_const [in Coq.micromega.ZMicromega]
Zeval_expr [in Coq.micromega.ZMicromega]
Zeven [in Coq.ZArith.Zeven]
Zeven_dec [in Coq.ZArith.Zeven]
Zeven_odd_dec [in Coq.ZArith.Zeven]
Zeven_odd_bool [in Coq.ZArith.Zbool]
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.setoid_ring.Ring_polynom]
zmon_pred [in Coq.micromega.EnvRing]
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]
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_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.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_inj_nat_rev [in Coq.Reals.Cauchy.ConstructiveExtra]
Z_inj_nat [in Coq.Reals.Cauchy.ConstructiveExtra]
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_comparison [in Coq.micromega.ZifyComparison]
Z_of_N' [in Coq.omega.PreOmega]
Z_of_nat' [in Coq.omega.PreOmega]
z_of_exp [in Coq.micromega.RMicromega]
z_of_int [in Coq.extraction.ExtrOcamlIntConv]
z_of_z [in Coq.Numbers.AltBinNotations]
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_num_int [in Coq.ZArith.BinIntDef]
Z.of_hex_int [in Coq.ZArith.BinIntDef]
Z.of_int [in Coq.ZArith.BinIntDef]
Z.of_num_uint [in Coq.ZArith.BinIntDef]
Z.of_hex_uint [in Coq.ZArith.BinIntDef]
Z.of_uint [in Coq.ZArith.BinIntDef]
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_num_int [in Coq.ZArith.BinIntDef]
Z.to_hex_int [in Coq.ZArith.BinIntDef]
Z.to_int [in Coq.ZArith.BinIntDef]
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 | (70451 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 | (1003 entries) |
| Binder 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 | (45703 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 | (771 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 | (1516 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 | (579 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 | (11670 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 | (1018 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 | (622 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 | (304 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 | (472 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 | (482 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 | (844 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 | (1187 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 | (4117 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 | (163 entries) |