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 (18818 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 (548 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 (206 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 (68 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 (8939 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)
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)
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)
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 (1243 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)
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 (2935 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 (703 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)
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 (408 entries)

N (axiom)

NAbstract.destr_t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.digits_dom_op [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.dom_t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.iter_mk_t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.iter_t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.mk_t_S_level [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.mk_t_S [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.mk_t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.reduce [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.same_level [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.spec_mk_t_S [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.spec_same_level_dep [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.spec_reduce [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.spec_mk_t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.t [in Coq.Numbers.Natural.BigN.Nbasic]
NAbstract.to_Z [in Coq.Numbers.Natural.BigN.Nbasic]
NAxiomsRec.recursion [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec.recursion_succ [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsRec.recursion_0 [in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiom.pred_0 [in Coq.Numbers.Natural.Abstract.NAxioms]
NDivSpecific.mod_upper_bound [in Coq.Numbers.Natural.Abstract.NAxioms]
NType_ZType.spec_Zabs_N [in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.Zabs_N [in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.spec_Z_of_N [in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.Z_of_N [in Coq.Numbers.Rational.BigQ.QMake]
NType.add [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.compare [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div_eucl [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div2 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.eqb [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.even [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.gcd [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.land [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.ldiff [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.leb [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.log2 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.lor [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.ltb [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.lxor [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.max [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.min [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.modulo [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.mul [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.odd [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.of_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.one [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.pow [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.pow_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.pow_pos [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.pred [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.shiftl [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.shiftr [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div2 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_lxor [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_ldiff [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_lor [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_land [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_shiftl [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_shiftr [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_testbit [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_odd [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_even [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_gcd [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_modulo [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div_eucl [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_log2 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sqrt [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pow [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pow_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pow_pos [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_square [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_mul [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sub [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pred [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_add [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_succ [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_2 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_1 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_0 [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_min [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_max [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_leb [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_ltb [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_eqb [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_compare [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_of_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pos [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.sqrt [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.square [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.sub [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.succ [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.t [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.testbit [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.to_Z [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.two [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.zero [in Coq.Numbers.Natural.SpecViaZ.NSig]
NZBitsSpec.div2_spec [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.land_spec [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.ldiff_spec [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.lor_spec [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.lxor_spec [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.shiftl_spec_low [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.shiftl_spec_high [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.shiftr_spec [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_neg_r [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_even_succ [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_odd_succ [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_even_0 [in Coq.Numbers.NatInt.NZBits]
NZBitsSpec.testbit_odd_0 [in Coq.Numbers.NatInt.NZBits]
NZDivSpec.div_mod [in Coq.Numbers.NatInt.NZDiv]
NZDivSpec.mod_bound_pos [in Coq.Numbers.NatInt.NZDiv]
NZGcdSpec.gcd_nonneg [in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_greatest [in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_divide_r [in Coq.Numbers.NatInt.NZGcd]
NZGcdSpec.gcd_divide_l [in Coq.Numbers.NatInt.NZGcd]
NZLog2Spec.log2_nonpos [in Coq.Numbers.NatInt.NZLog]
NZLog2Spec.log2_spec [in Coq.Numbers.NatInt.NZLog]
NZParity.even [in Coq.Numbers.NatInt.NZParity]
NZParity.even_spec [in Coq.Numbers.NatInt.NZParity]
NZParity.odd [in Coq.Numbers.NatInt.NZParity]
NZParity.odd_spec [in Coq.Numbers.NatInt.NZParity]
NZPowSpec.pow_neg_r [in Coq.Numbers.NatInt.NZPow]
NZPowSpec.pow_succ_r [in Coq.Numbers.NatInt.NZPow]
NZPowSpec.pow_0_r [in Coq.Numbers.NatInt.NZPow]
NZSqrtSpec.sqrt_neg [in Coq.Numbers.NatInt.NZSqrt]
NZSqrtSpec.sqrt_spec [in Coq.Numbers.NatInt.NZSqrt]
NZSquare.square [in Coq.Numbers.NatInt.NZAxioms]
NZSquare.square_spec [in Coq.Numbers.NatInt.NZAxioms]


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 (18818 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 (548 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 (206 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 (68 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 (8939 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)
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)
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)
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 (1243 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)
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 (2935 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 (703 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)
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 (408 entries)