| 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 | (22207 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 | (923 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 | (744 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 | (1482 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 | (500 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 | (10360 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 | (910 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 | (573 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 | (386 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 | (286 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 | (467 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 | (631 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 | (1123 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 | (3677 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 | (145 entries) |
O
O [constructor, in Coq.Init.Datatypes]oapp [abbreviation, in Coq.ssr.ssrfun]
obind [abbreviation, in Coq.ssr.ssrfun]
obligation [definition, in Coq.Program.Tactics]
ObsoletePmultNat [section, in Coq.PArith.Pnat]
ocancel [definition, in Coq.ssr.ssrfun]
OctalString [library]
odd [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
Odd [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
odd [definition, in Coq.Init.Nat]
odd [inductive, in Coq.Arith.Even]
odd_bitwise [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
Odd_equiv [lemma, in Coq.Numbers.Natural.Peano.NPeano]
odd_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
odd_even_lem [lemma, in Coq.Arith.Mult]
odd_S2n [lemma, in Coq.Arith.Div2]
odd_double [lemma, in Coq.Arith.Div2]
odd_div2 [lemma, in Coq.Arith.Div2]
odd_mult_inv_r [lemma, in Coq.Arith.Even]
odd_mult_inv_l [lemma, in Coq.Arith.Even]
odd_mult [lemma, in Coq.Arith.Even]
odd_plus_odd_inv_r [lemma, in Coq.Arith.Even]
odd_plus_odd_inv_l [lemma, in Coq.Arith.Even]
odd_plus_even_inv_r [lemma, in Coq.Arith.Even]
odd_plus_even_inv_l [lemma, in Coq.Arith.Even]
odd_even_plus [lemma, in Coq.Arith.Even]
odd_plus_r [lemma, in Coq.Arith.Even]
odd_plus_l [lemma, in Coq.Arith.Even]
odd_plus_split [lemma, in Coq.Arith.Even]
odd_equiv [lemma, in Coq.Arith.Even]
odd_S [constructor, in Coq.Arith.Even]
odflt [abbreviation, in Coq.ssr.ssrfun]
OEQ [constructor, in Coq.Structures.OrdersTac]
of_Z_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
of_pos_rec_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
of_to_Z [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
of_Z [definition, in Coq.Numbers.Cyclic.Int63.Int63]
of_pos [definition, in Coq.Numbers.Cyclic.Int63.Int63]
of_pos_rec [definition, in Coq.Numbers.Cyclic.Int63.Int63]
of_pos [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
of_nat_0 [definition, in Coq.Strings.BinaryString]
of_Z_m1 [definition, in Coq.Strings.BinaryString]
of_Z_0 [definition, in Coq.Strings.BinaryString]
of_N_0 [definition, in Coq.Strings.BinaryString]
of_pos_3 [definition, in Coq.Strings.BinaryString]
of_pos_2 [definition, in Coq.Strings.BinaryString]
of_pos_1 [definition, in Coq.Strings.BinaryString]
of_nat [definition, in Coq.Strings.BinaryString]
of_Z [definition, in Coq.Strings.BinaryString]
of_N [definition, in Coq.Strings.BinaryString]
of_pos [definition, in Coq.Strings.BinaryString]
of_bits_to_bits [lemma, in Coq.Init.Byte]
of_bits [definition, in Coq.Init.Byte]
of_nat_to_nat_inv [lemma, in Coq.Vectors.Fin]
of_nat_ext [lemma, in Coq.Vectors.Fin]
of_nat_lt [definition, in Coq.Vectors.Fin]
of_nat [definition, in Coq.Vectors.Fin]
of_int [definition, in Coq.Init.Nat]
of_uint [definition, in Coq.Init.Nat]
of_uint_acc [definition, in Coq.Init.Nat]
of_nat_0 [definition, in Coq.Strings.OctalString]
of_Z_m1 [definition, in Coq.Strings.OctalString]
of_Z_0 [definition, in Coq.Strings.OctalString]
of_N_0 [definition, in Coq.Strings.OctalString]
of_pos_8 [definition, in Coq.Strings.OctalString]
of_pos_7 [definition, in Coq.Strings.OctalString]
of_pos_3 [definition, in Coq.Strings.OctalString]
of_pos_2 [definition, in Coq.Strings.OctalString]
of_pos_1 [definition, in Coq.Strings.OctalString]
of_nat [definition, in Coq.Strings.OctalString]
of_Z [definition, in Coq.Strings.OctalString]
of_N [definition, in Coq.Strings.OctalString]
of_pos [definition, in Coq.Strings.OctalString]
of_nat_via_N [lemma, in Coq.Strings.Byte]
of_N_via_nat [lemma, in Coq.Strings.Byte]
of_N_None_iff [lemma, in Coq.Strings.Byte]
of_to_N [lemma, in Coq.Strings.Byte]
of_N [definition, in Coq.Strings.Byte]
of_nat_None_iff [lemma, in Coq.Strings.Byte]
of_to_nat [lemma, in Coq.Strings.Byte]
of_nat [definition, in Coq.Strings.Byte]
of_nat_0 [definition, in Coq.Strings.HexString]
of_Z_m1 [definition, in Coq.Strings.HexString]
of_Z_0 [definition, in Coq.Strings.HexString]
of_N_0 [definition, in Coq.Strings.HexString]
of_pos_16 [definition, in Coq.Strings.HexString]
of_pos_15 [definition, in Coq.Strings.HexString]
of_pos_14 [definition, in Coq.Strings.HexString]
of_pos_13 [definition, in Coq.Strings.HexString]
of_pos_12 [definition, in Coq.Strings.HexString]
of_pos_11 [definition, in Coq.Strings.HexString]
of_pos_10 [definition, in Coq.Strings.HexString]
of_pos_9 [definition, in Coq.Strings.HexString]
of_pos_8 [definition, in Coq.Strings.HexString]
of_pos_7 [definition, in Coq.Strings.HexString]
of_pos_3 [definition, in Coq.Strings.HexString]
of_pos_2 [definition, in Coq.Strings.HexString]
of_pos_1 [definition, in Coq.Strings.HexString]
of_nat [definition, in Coq.Strings.HexString]
of_Z [definition, in Coq.Strings.HexString]
of_N [definition, in Coq.Strings.HexString]
of_pos [definition, in Coq.Strings.HexString]
of_list [definition, in Coq.Vectors.VectorDef]
of_Bvector [definition, in Coq.Strings.ByteVector]
of_string [definition, in Coq.Strings.ByteVector]
of_decimal [definition, in Coq.QArith.QArith_base]
of_iff [lemma, in Coq.Numbers.DecimalZ]
of_inj [lemma, in Coq.Numbers.DecimalZ]
of_int_norm [lemma, in Coq.Numbers.DecimalZ]
of_to [lemma, in Coq.Numbers.DecimalZ]
OLE [constructor, in Coq.Structures.OrdersTac]
OLT [constructor, in Coq.Structures.OrdersTac]
omap [abbreviation, in Coq.ssr.ssrfun]
Omega [library]
OmegaLemmas [library]
OmegaPlugin [library]
OmegaTactic [library]
OMEGA1 [lemma, in Coq.omega.OmegaLemmas]
OMEGA10 [lemma, in Coq.omega.OmegaLemmas]
OMEGA11 [lemma, in Coq.omega.OmegaLemmas]
OMEGA12 [lemma, in Coq.omega.OmegaLemmas]
OMEGA13 [lemma, in Coq.omega.OmegaLemmas]
OMEGA14 [lemma, in Coq.omega.OmegaLemmas]
OMEGA15 [lemma, in Coq.omega.OmegaLemmas]
OMEGA16 [lemma, in Coq.omega.OmegaLemmas]
OMEGA17 [lemma, in Coq.omega.OmegaLemmas]
OMEGA18 [lemma, in Coq.omega.OmegaLemmas]
OMEGA19 [lemma, in Coq.omega.OmegaLemmas]
OMEGA2 [lemma, in Coq.omega.OmegaLemmas]
OMEGA20 [lemma, in Coq.omega.OmegaLemmas]
OMEGA3 [lemma, in Coq.omega.OmegaLemmas]
OMEGA4 [lemma, in Coq.omega.OmegaLemmas]
OMEGA5 [lemma, in Coq.omega.OmegaLemmas]
OMEGA6 [lemma, in Coq.omega.OmegaLemmas]
OMEGA7 [lemma, in Coq.omega.OmegaLemmas]
OMEGA8 [lemma, in Coq.omega.OmegaLemmas]
OMEGA9 [lemma, in Coq.omega.OmegaLemmas]
OmniscientFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
OmniscientFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice_on [definition, in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_small_drinker [lemma, in Coq.Logic.ChoiceFacts]
On [definition, in Coq.Numbers.Cyclic.Int31.Int31]
one [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
one [definition, in Coq.Init.Nat]
one [definition, in Coq.Strings.Ascii]
one [projection, in Coq.setoid_ring.Algebra_syntax]
One [record, in Coq.setoid_ring.Algebra_syntax]
one [constructor, in Coq.setoid_ring.Algebra_syntax]
One [inductive, in Coq.setoid_ring.Algebra_syntax]
OneTwo [module, in Coq.Numbers.NatInt.NZAxioms]
OneTwoNotation [module, in Coq.Numbers.NatInt.NZAxioms]
1 [notation, in Coq.Numbers.NatInt.NZAxioms]
2 [notation, in Coq.Numbers.NatInt.NZAxioms]
OneTwo' [module, in Coq.Numbers.NatInt.NZAxioms]
OneTwo.one [axiom, in Coq.Numbers.NatInt.NZAxioms]
OneTwo.two [axiom, in Coq.Numbers.NatInt.NZAxioms]
one_IZR_r_R1 [lemma, in Coq.Reals.RIneq]
one_IZR_lt1 [lemma, in Coq.Reals.RIneq]
one_notation [instance, in Coq.setoid_ring.Ncring]
onPhantom [definition, in Coq.ssr.ssrbool]
onT_bij [lemma, in Coq.ssr.ssrbool]
onW_bij [lemma, in Coq.ssr.ssrbool]
on_can_inj [lemma, in Coq.ssr.ssrbool]
on1lT [lemma, in Coq.ssr.ssrbool]
on1lW [lemma, in Coq.ssr.ssrbool]
on1T [lemma, in Coq.ssr.ssrbool]
on1W [lemma, in Coq.ssr.ssrbool]
on2T [lemma, in Coq.ssr.ssrbool]
on2W [lemma, in Coq.ssr.ssrbool]
OpAdd [definition, in Coq.micromega.RingMicromega]
OpAdd_sound [lemma, in Coq.micromega.RingMicromega]
open_interval [definition, in Coq.Reals.RiemannInt_SF]
open_set_P6 [lemma, in Coq.Reals.Rtopology]
open_set_P5 [lemma, in Coq.Reals.Rtopology]
open_set_P4 [lemma, in Coq.Reals.Rtopology]
open_set_P3 [lemma, in Coq.Reals.Rtopology]
open_set_P2 [lemma, in Coq.Reals.Rtopology]
open_set_P1 [lemma, in Coq.Reals.Rtopology]
open_set [definition, in Coq.Reals.Rtopology]
OpEq [constructor, in Coq.micromega.RingMicromega]
OperationProperties [section, in Coq.ssr.ssrfun]
OperationProperties.R [variable, in Coq.ssr.ssrfun]
OperationProperties.S [variable, in Coq.ssr.ssrfun]
OperationProperties.SopSisS [section, in Coq.ssr.ssrfun]
OperationProperties.SopSisT [section, in Coq.ssr.ssrfun]
OperationProperties.SopTisR [section, in Coq.ssr.ssrfun]
OperationProperties.SopTisS [section, in Coq.ssr.ssrfun]
OperationProperties.SopTisT [section, in Coq.ssr.ssrfun]
OperationProperties.T [variable, in Coq.ssr.ssrfun]
Operators_Properties [library]
OpGe [constructor, in Coq.micromega.RingMicromega]
OpGt [constructor, in Coq.micromega.RingMicromega]
OpLe [constructor, in Coq.micromega.RingMicromega]
OpLt [constructor, in Coq.micromega.RingMicromega]
OpMult [definition, in Coq.micromega.RingMicromega]
OpMult_sound [lemma, in Coq.micromega.RingMicromega]
OpNEq [constructor, in Coq.micromega.RingMicromega]
Opp [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
opp [definition, in Coq.Numbers.Cyclic.Int63.Int63]
opp [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp [definition, in Coq.Init.Decimal]
oppc [definition, in Coq.Numbers.Cyclic.Int63.Int63]
oppcarry [definition, in Coq.Numbers.Cyclic.Int63.Int63]
oppcarry_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
OppCstNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
- 2 [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
- 1 [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
oppc_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
OppNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
- _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
opposite [projection, in Coq.setoid_ring.Algebra_syntax]
Opposite [record, in Coq.setoid_ring.Algebra_syntax]
opposite [constructor, in Coq.setoid_ring.Algebra_syntax]
Opposite [inductive, in Coq.setoid_ring.Algebra_syntax]
opp_IZR [lemma, in Coq.Reals.RIneq]
opp_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
opp_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_fct [definition, in Coq.Reals.Ranalysis1]
opp_notation [instance, in Coq.setoid_ring.Ncring]
opp_seq [definition, in Coq.Reals.SeqProp]
Opp' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Opp.opp [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
opp31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Ops [module, in Coq.MSets.MSetRBT]
Ops [module, in Coq.MSets.MSetWeakList]
Ops [module, in Coq.MSets.MSetInterface]
Ops [module, in Coq.MSets.MSetList]
Ops [module, in Coq.MSets.MSetGenTree]
Ops [module, in Coq.MSets.MSetAVL]
Ops.add [definition, in Coq.MSets.MSetRBT]
Ops.add [definition, in Coq.MSets.MSetWeakList]
Ops.add [definition, in Coq.MSets.MSetList]
Ops.add [definition, in Coq.MSets.MSetAVL]
Ops.append [definition, in Coq.MSets.MSetRBT]
Ops.assert_false [definition, in Coq.MSets.MSetAVL]
Ops.bal [definition, in Coq.MSets.MSetAVL]
Ops.Bk [abbreviation, in Coq.MSets.MSetRBT]
Ops.bogus [definition, in Coq.MSets.MSetRBT]
Ops.cardinal [definition, in Coq.MSets.MSetWeakList]
Ops.cardinal [definition, in Coq.MSets.MSetList]
Ops.cardinal [definition, in Coq.MSets.MSetGenTree]
Ops.choose [definition, in Coq.MSets.MSetWeakList]
Ops.choose [definition, in Coq.MSets.MSetList]
Ops.choose [definition, in Coq.MSets.MSetGenTree]
Ops.compare [definition, in Coq.MSets.MSetList]
Ops.compare [definition, in Coq.MSets.MSetGenTree]
Ops.compare_height [definition, in Coq.MSets.MSetRBT]
Ops.compare_end [definition, in Coq.MSets.MSetGenTree]
Ops.compare_cont [definition, in Coq.MSets.MSetGenTree]
Ops.compare_more [definition, in Coq.MSets.MSetGenTree]
Ops.concat [definition, in Coq.MSets.MSetAVL]
Ops.cons [definition, in Coq.MSets.MSetGenTree]
Ops.create [definition, in Coq.MSets.MSetAVL]
Ops.del [definition, in Coq.MSets.MSetRBT]
Ops.delmin [definition, in Coq.MSets.MSetRBT]
Ops.diff [definition, in Coq.MSets.MSetRBT]
Ops.diff [definition, in Coq.MSets.MSetWeakList]
Ops.diff [definition, in Coq.MSets.MSetList]
Ops.diff [definition, in Coq.MSets.MSetAVL]
Ops.diff_list [definition, in Coq.MSets.MSetRBT]
Ops.elements [definition, in Coq.MSets.MSetWeakList]
Ops.elements [definition, in Coq.MSets.MSetList]
Ops.elements [definition, in Coq.MSets.MSetGenTree]
Ops.elements_aux [definition, in Coq.MSets.MSetGenTree]
Ops.elt [definition, in Coq.MSets.MSetWeakList]
Ops.elt [definition, in Coq.MSets.MSetList]
Ops.elt [definition, in Coq.MSets.MSetGenTree]
Ops.empty [definition, in Coq.MSets.MSetWeakList]
Ops.empty [definition, in Coq.MSets.MSetList]
Ops.empty [definition, in Coq.MSets.MSetGenTree]
Ops.End [constructor, in Coq.MSets.MSetGenTree]
Ops.enumeration [inductive, in Coq.MSets.MSetGenTree]
Ops.equal [definition, in Coq.MSets.MSetWeakList]
Ops.equal [definition, in Coq.MSets.MSetList]
Ops.equal [definition, in Coq.MSets.MSetGenTree]
Ops.exists_ [definition, in Coq.MSets.MSetWeakList]
Ops.exists_ [definition, in Coq.MSets.MSetList]
Ops.exists_ [definition, in Coq.MSets.MSetGenTree]
Ops.filter [definition, in Coq.MSets.MSetRBT]
Ops.filter [definition, in Coq.MSets.MSetWeakList]
Ops.filter [definition, in Coq.MSets.MSetList]
Ops.filter [definition, in Coq.MSets.MSetAVL]
Ops.filter_aux [definition, in Coq.MSets.MSetRBT]
Ops.fold [definition, in Coq.MSets.MSetWeakList]
Ops.fold [definition, in Coq.MSets.MSetList]
Ops.fold [definition, in Coq.MSets.MSetGenTree]
Ops.for_all [definition, in Coq.MSets.MSetWeakList]
Ops.for_all [definition, in Coq.MSets.MSetList]
Ops.for_all [definition, in Coq.MSets.MSetGenTree]
Ops.height [definition, in Coq.MSets.MSetAVL]
Ops.ins [definition, in Coq.MSets.MSetRBT]
Ops.int [abbreviation, in Coq.MSets.MSetAVL]
Ops.inter [definition, in Coq.MSets.MSetRBT]
Ops.inter [definition, in Coq.MSets.MSetWeakList]
Ops.inter [definition, in Coq.MSets.MSetList]
Ops.inter [definition, in Coq.MSets.MSetAVL]
Ops.inter_list [definition, in Coq.MSets.MSetRBT]
Ops.is_empty [definition, in Coq.MSets.MSetWeakList]
Ops.is_empty [definition, in Coq.MSets.MSetList]
Ops.is_empty [definition, in Coq.MSets.MSetGenTree]
Ops.join [definition, in Coq.MSets.MSetAVL]
Ops.lbal [definition, in Coq.MSets.MSetRBT]
Ops.lbalS [definition, in Coq.MSets.MSetRBT]
Ops.Leaf [constructor, in Coq.MSets.MSetGenTree]
Ops.linear_diff [definition, in Coq.MSets.MSetRBT]
Ops.linear_inter [definition, in Coq.MSets.MSetRBT]
Ops.linear_union [definition, in Coq.MSets.MSetRBT]
Ops.makeBlack [definition, in Coq.MSets.MSetRBT]
Ops.makeRed [definition, in Coq.MSets.MSetRBT]
Ops.maxdepth [definition, in Coq.MSets.MSetGenTree]
Ops.max_elt [definition, in Coq.MSets.MSetList]
Ops.max_elt [definition, in Coq.MSets.MSetGenTree]
Ops.mem [definition, in Coq.MSets.MSetWeakList]
Ops.mem [definition, in Coq.MSets.MSetList]
Ops.mem [definition, in Coq.MSets.MSetGenTree]
Ops.merge [definition, in Coq.MSets.MSetAVL]
Ops.mindepth [definition, in Coq.MSets.MSetGenTree]
Ops.min_elt [definition, in Coq.MSets.MSetList]
Ops.min_elt [definition, in Coq.MSets.MSetGenTree]
Ops.mktriple [constructor, in Coq.MSets.MSetAVL]
Ops.More [constructor, in Coq.MSets.MSetGenTree]
Ops.Node [constructor, in Coq.MSets.MSetGenTree]
Ops.partition [definition, in Coq.MSets.MSetRBT]
Ops.partition [definition, in Coq.MSets.MSetWeakList]
Ops.partition [definition, in Coq.MSets.MSetList]
Ops.partition [definition, in Coq.MSets.MSetAVL]
Ops.partition_aux [definition, in Coq.MSets.MSetRBT]
Ops.plength [definition, in Coq.MSets.MSetRBT]
Ops.plength_aux [definition, in Coq.MSets.MSetRBT]
Ops.rbal [definition, in Coq.MSets.MSetRBT]
Ops.rbalS [definition, in Coq.MSets.MSetRBT]
Ops.rbal' [definition, in Coq.MSets.MSetRBT]
Ops.Rd [abbreviation, in Coq.MSets.MSetRBT]
Ops.remove [definition, in Coq.MSets.MSetRBT]
Ops.remove [definition, in Coq.MSets.MSetWeakList]
Ops.remove [definition, in Coq.MSets.MSetList]
Ops.remove [definition, in Coq.MSets.MSetAVL]
Ops.remove_min [definition, in Coq.MSets.MSetRBT]
Ops.remove_min [definition, in Coq.MSets.MSetAVL]
Ops.rev_elements [definition, in Coq.MSets.MSetGenTree]
Ops.rev_elements_aux [definition, in Coq.MSets.MSetGenTree]
Ops.singleton [definition, in Coq.MSets.MSetRBT]
Ops.singleton [definition, in Coq.MSets.MSetWeakList]
Ops.singleton [definition, in Coq.MSets.MSetList]
Ops.singleton [definition, in Coq.MSets.MSetAVL]
Ops.skip_black [definition, in Coq.MSets.MSetRBT]
Ops.skip_red [definition, in Coq.MSets.MSetRBT]
Ops.split [definition, in Coq.MSets.MSetAVL]
Ops.subset [definition, in Coq.MSets.MSetWeakList]
Ops.subset [definition, in Coq.MSets.MSetList]
Ops.subset [definition, in Coq.MSets.MSetGenTree]
Ops.subsetl [definition, in Coq.MSets.MSetGenTree]
Ops.subsetr [definition, in Coq.MSets.MSetGenTree]
Ops.t [definition, in Coq.MSets.MSetRBT]
Ops.t [definition, in Coq.MSets.MSetWeakList]
Ops.t [definition, in Coq.MSets.MSetList]
Ops.t [definition, in Coq.MSets.MSetAVL]
Ops.tree [inductive, in Coq.MSets.MSetGenTree]
Ops.treeify [definition, in Coq.MSets.MSetRBT]
Ops.treeify_aux [definition, in Coq.MSets.MSetRBT]
Ops.treeify_cont [definition, in Coq.MSets.MSetRBT]
Ops.treeify_one [definition, in Coq.MSets.MSetRBT]
Ops.treeify_zero [definition, in Coq.MSets.MSetRBT]
Ops.treeify_t [abbreviation, in Coq.MSets.MSetRBT]
Ops.triple [record, in Coq.MSets.MSetAVL]
Ops.t_right [projection, in Coq.MSets.MSetAVL]
Ops.t_in [projection, in Coq.MSets.MSetAVL]
Ops.t_left [projection, in Coq.MSets.MSetAVL]
Ops.union [definition, in Coq.MSets.MSetRBT]
Ops.union [definition, in Coq.MSets.MSetWeakList]
Ops.union [definition, in Coq.MSets.MSetList]
Ops.union [definition, in Coq.MSets.MSetAVL]
Ops.union_list [definition, in Coq.MSets.MSetRBT]
<< _ , _ , _ >> [notation, in Coq.MSets.MSetAVL]
Option [module, in Coq.ssr.ssrfun]
option [inductive, in Coq.Init.Datatypes]
option_map [definition, in Coq.Init.Datatypes]
Option.apply [definition, in Coq.ssr.ssrfun]
Option.bind [definition, in Coq.ssr.ssrfun]
Option.default [definition, in Coq.ssr.ssrfun]
Option.map [definition, in Coq.ssr.ssrfun]
op_rotate [lemma, in Coq.Sets.Permut]
Op1 [inductive, in Coq.micromega.RingMicromega]
Op2 [inductive, in Coq.micromega.RingMicromega]
or [inductive, in Coq.Init.Logic]
orb [definition, in Coq.Init.Datatypes]
orbA [lemma, in Coq.ssr.ssrbool]
orbAC [lemma, in Coq.ssr.ssrbool]
orbACA [lemma, in Coq.ssr.ssrbool]
orbb [lemma, in Coq.ssr.ssrbool]
orbC [lemma, in Coq.ssr.ssrbool]
orbCA [lemma, in Coq.ssr.ssrbool]
orbF [lemma, in Coq.ssr.ssrbool]
orbK [lemma, in Coq.ssr.ssrbool]
orbN [lemma, in Coq.ssr.ssrbool]
orbT [lemma, in Coq.ssr.ssrbool]
orb_id2r [lemma, in Coq.ssr.ssrbool]
orb_id2l [lemma, in Coq.ssr.ssrbool]
orb_idr [lemma, in Coq.ssr.ssrbool]
orb_idl [lemma, in Coq.ssr.ssrbool]
orb_andr [lemma, in Coq.ssr.ssrbool]
orb_andl [lemma, in Coq.ssr.ssrbool]
orb_lazy_alt [lemma, in Coq.Bool.Bool]
orb_prop_intro [lemma, in Coq.Bool.Bool]
orb_prop2 [abbreviation, in Coq.Bool.Bool]
orb_prop_elim [lemma, in Coq.Bool.Bool]
orb_andb_distrib_l [lemma, in Coq.Bool.Bool]
orb_andb_distrib_r [lemma, in Coq.Bool.Bool]
orb_assoc [lemma, in Coq.Bool.Bool]
orb_comm [lemma, in Coq.Bool.Bool]
orb_neg_b [abbreviation, in Coq.Bool.Bool]
orb_negb_r [lemma, in Coq.Bool.Bool]
orb_false_b [abbreviation, in Coq.Bool.Bool]
orb_b_false [abbreviation, in Coq.Bool.Bool]
orb_false_l [lemma, in Coq.Bool.Bool]
orb_false_r [lemma, in Coq.Bool.Bool]
orb_true_b [abbreviation, in Coq.Bool.Bool]
orb_b_true [abbreviation, in Coq.Bool.Bool]
orb_true_l [lemma, in Coq.Bool.Bool]
orb_true_r [lemma, in Coq.Bool.Bool]
orb_diag [lemma, in Coq.Bool.Bool]
orb_false_elim [lemma, in Coq.Bool.Bool]
orb_false_intro [lemma, in Coq.Bool.Bool]
orb_true_intro [lemma, in Coq.Bool.Bool]
orb_prop [lemma, in Coq.Bool.Bool]
orb_true_elim [lemma, in Coq.Bool.Bool]
orb_false_iff [lemma, in Coq.Bool.Bool]
orb_true_iff [lemma, in Coq.Bool.Bool]
ord [inductive, in Coq.Structures.OrdersTac]
Order [inductive, in Coq.Sets.Relations_1]
order [record, in Coq.Relations.Relation_Definitions]
OrderedRing [library]
OrderedRingSyntax [module, in Coq.micromega.OrderedRing]
OrderedType [module, in Coq.Structures.Orders]
OrderedType [module, in Coq.Structures.OrderedType]
OrderedType [library]
OrderedTypeAlt [module, in Coq.Structures.OrdersAlt]
OrderedTypeAlt [module, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt [library]
OrderedTypeAlt.compare [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.t [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.t [axiom, in Coq.Structures.OrderedTypeAlt]
_ ?= _ [notation, in Coq.Structures.OrdersAlt]
_ ?= _ [notation, in Coq.Structures.OrderedTypeAlt]
OrderedTypeEx [library]
OrderedTypeFacts [module, in Coq.Structures.OrderedType]
OrderedTypeFacts [module, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.compare_ge_iff [abbreviation, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.compare_le_iff [abbreviation, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.elim_compare_gt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.elim_compare_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.elim_compare_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eqb_alt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eqb_alt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_dec [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_not_gt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_not_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_neq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_le [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_equiv [instance, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_dec [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_trans [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_sym [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_refl [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.ForNotations [section, in Coq.Structures.OrderedType]
OrderedTypeFacts.gt_not_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.if_eq_dec [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.In [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_alt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.In_Inf [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.In_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO [module, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.eq_equiv [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.le_lteq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_total [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_compat [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_strorder [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_antisym [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_trans [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_neq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_lt_trans [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.ListIn_Inf [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.ListIn_In [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_dec [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_not_gt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_le [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_le_trans [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_total [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_compat [instance, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_strorder [instance, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_antirefl [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_dec [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.lt_irrefl [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.lt_trans [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.neq_sym [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.neq_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.NoDup [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.OrderTac [module, in Coq.Structures.OrderedType]
OrderedTypeFacts.OrderTac [module, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.Sort [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.Sort_NoDup [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.Sort_Inf_In [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO [module, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.eq [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.le [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.lt [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.t [definition, in Coq.Structures.OrderedType]
_ ?= _ (order) [notation, in Coq.Structures.OrdersFacts]
_ <= _ (order) [notation, in Coq.Structures.OrdersFacts]
OrderedTypeFull [module, in Coq.Structures.Orders]
OrderedTypeFullFacts [module, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.compare_ge_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.compare_le_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.eq_is_le_ge [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_or_gt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_not_gt_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_antisym [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_order [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_preorder [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_or_ge [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_not_ge_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.OrderTac [module, in Coq.Structures.OrdersFacts]
OrderedTypeFull' [module, in Coq.Structures.Orders]
OrderedTypeLists [module, in Coq.Structures.OrdersLists]
OrderedTypeLists.In [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_alt [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_eq [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_lt [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.In_Inf [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.In_eq [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.ListIn_Inf [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.ListIn_In [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.NoDup [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort_NoDup [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort_Inf_In [lemma, in Coq.Structures.OrdersLists]
OrderedTypeOrig [module, in Coq.Structures.OrdersAlt]
OrderedTypeRev [module, in Coq.Structures.OrdersFacts]
OrderedTypeRev.compare [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.compare_spec [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq_dec [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq_equiv [instance, in Coq.Structures.OrdersFacts]
OrderedTypeRev.le [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.le_lteq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt_strorder [instance, in Coq.Structures.OrdersFacts]
OrderedTypeRev.t [definition, in Coq.Structures.OrdersFacts]
OrderedTypeTest [module, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_is_nlt_ngt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_not_gt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_not_lt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_neq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_le [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_lt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.gt_not_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_neq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_antisym [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_trans [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_lt_trans [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_not_gt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_le [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_le_trans [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_not_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.MO [module, in Coq.Structures.OrdersFacts]
OrderedTypeTest.neq_sym [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.neq_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeWithLeibniz [module, in Coq.MSets.MSetList]
OrderedTypeWithLeibniz.eq_leibniz [axiom, in Coq.MSets.MSetList]
OrderedType_to_Alt.compare_trans [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.compare_sym [lemma, in Coq.Structures.OrderedTypeAlt]
_ ?= _ [notation, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.compare [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.t [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.MO [module, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt [module, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_dec [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.compare [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_not_eq [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_trans [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_trans [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_sym [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_refl [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.t [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt [module, in Coq.Structures.OrderedTypeAlt]
OrderedType' [module, in Coq.Structures.Orders]
OrderedType.eq_dec [axiom, in Coq.Structures.OrderedType]
ordered_Rlist [definition, in Coq.Reals.RList]
OrderFacts [module, in Coq.Structures.OrdersTac]
OrderFacts.eq_neq [lemma, in Coq.Structures.OrdersTac]
OrderFacts.eq_le [definition, in Coq.Structures.OrdersTac]
OrderFacts.eq_lt [definition, in Coq.Structures.OrdersTac]
OrderFacts.eq_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.eq_sym [lemma, in Coq.Structures.OrdersTac]
OrderFacts.eq_refl [lemma, in Coq.Structures.OrdersTac]
OrderFacts.interp_ord [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_neq_lt [lemma, in Coq.Structures.OrdersTac]
OrderFacts.le_eq [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_lt_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_antisym [lemma, in Coq.Structures.OrdersTac]
OrderFacts.le_refl [lemma, in Coq.Structures.OrdersTac]
OrderFacts.lt_eq [definition, in Coq.Structures.OrdersTac]
OrderFacts.lt_le_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.lt_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.lt_irrefl [lemma, in Coq.Structures.OrdersTac]
OrderFacts.neq_eq [lemma, in Coq.Structures.OrdersTac]
OrderFacts.neq_sym [lemma, in Coq.Structures.OrdersTac]
OrderFacts.not_gt_le [lemma, in Coq.Structures.OrdersTac]
OrderFacts.not_ge_lt [lemma, in Coq.Structures.OrdersTac]
OrderFacts.not_neq_eq [lemma, in Coq.Structures.OrdersTac]
OrderFacts.trans [lemma, in Coq.Structures.OrdersTac]
# [notation, in Coq.Structures.OrdersTac]
OrderFunctions [module, in Coq.Structures.Orders]
OrderFunctions' [module, in Coq.Structures.Orders]
Orders [library]
OrdersAlt [library]
OrdersEx [library]
OrdersFacts [library]
OrdersLists [library]
OrdersTac [library]
OrdProperties [module, in Coq.FSets.FMapFacts]
OrdProperties [module, in Coq.MSets.MSetProperties]
OrdProperties [module, in Coq.FSets.FSetProperties]
OrdProperties.Above [definition, in Coq.FSets.FMapFacts]
OrdProperties.Above [definition, in Coq.MSets.MSetProperties]
OrdProperties.Above [definition, in Coq.FSets.FSetProperties]
OrdProperties.Add [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.add_fold [lemma, in Coq.MSets.MSetProperties]
OrdProperties.add_fold [lemma, in Coq.FSets.FSetProperties]
OrdProperties.Below [definition, in Coq.FSets.FMapFacts]
OrdProperties.Below [definition, in Coq.MSets.MSetProperties]
OrdProperties.Below [definition, in Coq.FSets.FSetProperties]
OrdProperties.cardinal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.choose_equal [lemma, in Coq.MSets.MSetProperties]
OrdProperties.choose_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Equal_eqlistA [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_split [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_ge [definition, in Coq.FSets.FMapFacts]
OrdProperties.elements_lt [definition, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_Add_Above [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_Add [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_split [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_ge [definition, in Coq.MSets.MSetProperties]
OrdProperties.elements_lt [definition, in Coq.MSets.MSetProperties]
OrdProperties.elements_Add_Below [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add_Above [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_split [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_ge [definition, in Coq.FSets.FSetProperties]
OrdProperties.elements_lt [definition, in Coq.FSets.FSetProperties]
OrdProperties.Elt [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Elements [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.elt [variable, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Fold_properties [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Induction_Principles [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Min_Max_Elt [section, in Coq.FSets.FMapFacts]
OrdProperties.eqk [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.eqke [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.Equal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.FoldOpt [section, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt [section, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.FSets.FSetProperties]
OrdProperties.fold_Add_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_Add_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_Equal [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_equal [lemma, in Coq.MSets.MSetProperties]
OrdProperties.fold_4 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.fold_3 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.fold_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.fold_4 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.fold_3 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb [definition, in Coq.FSets.FMapFacts]
OrdProperties.gtb [definition, in Coq.MSets.MSetProperties]
OrdProperties.gtb [definition, in Coq.FSets.FSetProperties]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FMapFacts]
OrdProperties.gtb_1 [lemma, in Coq.FSets.FMapFacts]
OrdProperties.gtb_compat [instance, in Coq.MSets.MSetProperties]
OrdProperties.gtb_1 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb_1 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb [definition, in Coq.FSets.FMapFacts]
OrdProperties.leb [definition, in Coq.MSets.MSetProperties]
OrdProperties.leb [definition, in Coq.FSets.FSetProperties]
OrdProperties.leb_compat [lemma, in Coq.FSets.FMapFacts]
OrdProperties.leb_1 [lemma, in Coq.FSets.FMapFacts]
OrdProperties.leb_compat [instance, in Coq.MSets.MSetProperties]
OrdProperties.leb_1 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.leb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb_1 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.ltk [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.map_induction_min [lemma, in Coq.FSets.FMapFacts]
OrdProperties.map_induction_max [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Empty [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_MapsTo [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt [definition, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_aux [definition, in Coq.FSets.FMapFacts]
OrdProperties.ME [module, in Coq.FSets.FMapFacts]
OrdProperties.ME [module, in Coq.MSets.MSetProperties]
OrdProperties.ME [module, in Coq.FSets.FSetProperties]
OrdProperties.min_elt_Empty [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_MapsTo [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt [definition, in Coq.FSets.FMapFacts]
OrdProperties.ML [module, in Coq.MSets.MSetProperties]
OrdProperties.O [module, in Coq.FSets.FMapFacts]
OrdProperties.P [module, in Coq.FSets.FMapFacts]
OrdProperties.P [module, in Coq.MSets.MSetProperties]
OrdProperties.P [module, in Coq.FSets.FSetProperties]
OrdProperties.remove_fold_2 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.remove_fold_2 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.MSets.MSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.MSets.MSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FMapFacts]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.MSets.MSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FSetProperties]
ord_antisym [projection, in Coq.Relations.Relation_Definitions]
ord_trans [projection, in Coq.Relations.Relation_Definitions]
ord_refl [projection, in Coq.Relations.Relation_Definitions]
orFb [lemma, in Coq.ssr.ssrbool]
orKb [lemma, in Coq.ssr.ssrbool]
orNb [lemma, in Coq.ssr.ssrbool]
orP [lemma, in Coq.ssr.ssrbool]
orTb [lemma, in Coq.ssr.ssrbool]
or_not_and [lemma, in Coq.Logic.Classical_Prop]
or_to_imply [lemma, in Coq.Logic.Classical_Prop]
or_not_r_iff_2 [lemma, in Coq.Logic.Decidable]
or_not_r_iff_1 [lemma, in Coq.Logic.Decidable]
or_not_l_iff_2 [lemma, in Coq.Logic.Decidable]
or_not_l_iff_1 [lemma, in Coq.Logic.Decidable]
or_assoc [lemma, in Coq.Init.Logic]
or_comm [lemma, in Coq.Init.Logic]
or_cancel_r [lemma, in Coq.Init.Logic]
or_cancel_l [lemma, in Coq.Init.Logic]
or_iff_compat_r [lemma, in Coq.Init.Logic]
or_iff_compat_l [lemma, in Coq.Init.Logic]
or_intror [constructor, in Coq.Init.Logic]
or_introl [constructor, in Coq.Init.Logic]
or_indd [definition, in Coq.Logic.ClassicalFacts]
or_elim_redr [definition, in Coq.Logic.ClassicalFacts]
or_elim_redl [definition, in Coq.Logic.ClassicalFacts]
or_iff_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_impl_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_cnf_correct [lemma, in Coq.micromega.Tauto]
or_clause_cnf_correct [lemma, in Coq.micromega.Tauto]
or_clause_correct [lemma, in Coq.micromega.Tauto]
or_cnf [definition, in Coq.micromega.Tauto]
or_clause_cnf [definition, in Coq.micromega.Tauto]
or_clause [definition, in Coq.micromega.Tauto]
or3 [inductive, in Coq.ssr.ssrbool]
or3P [lemma, in Coq.ssr.ssrbool]
Or31 [constructor, in Coq.ssr.ssrbool]
Or32 [constructor, in Coq.ssr.ssrbool]
Or33 [constructor, in Coq.ssr.ssrbool]
or4 [inductive, in Coq.ssr.ssrbool]
or4P [lemma, in Coq.ssr.ssrbool]
Or41 [constructor, in Coq.ssr.ssrbool]
Or42 [constructor, in Coq.ssr.ssrbool]
Or43 [constructor, in Coq.ssr.ssrbool]
Or44 [constructor, in Coq.ssr.ssrbool]
OTF_to_TTLB.t [definition, in Coq.Structures.Orders]
OTF_to_TTLB.leb_trans [lemma, in Coq.Structures.Orders]
OTF_to_TTLB.leb_total [lemma, in Coq.Structures.Orders]
OTF_to_TTLB.leb_le [lemma, in Coq.Structures.Orders]
OTF_to_TTLB.leb [definition, in Coq.Structures.Orders]
OTF_to_TTLB [module, in Coq.Structures.Orders]
OTF_to_TotalOrder [module, in Coq.Structures.Orders]
OTF_LtIsTotal.lt_total [lemma, in Coq.Structures.Orders]
OTF_LtIsTotal [module, in Coq.Structures.Orders]
OTF_to_OrderTac.TO [module, in Coq.Structures.OrdersTac]
OTF_to_OrderTac [module, in Coq.Structures.OrdersTac]
other_definitions [section, in Coq.Lists.ListSet]
OT_to_Full.le_lteq [lemma, in Coq.Structures.Orders]
OT_to_Full.le [definition, in Coq.Structures.Orders]
OT_to_Full [module, in Coq.Structures.Orders]
OT_to_Alt.compare_trans [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Gt [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Lt [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Eq [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_sym [lemma, in Coq.Structures.OrdersAlt]
_ ?= _ [notation, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare [definition, in Coq.Structures.OrdersAlt]
OT_to_Alt.t [definition, in Coq.Structures.OrdersAlt]
OT_to_Alt [module, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_dec [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.compare_spec [lemma, in Coq.Structures.OrdersAlt]
OT_from_Alt.compare [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_compat [instance, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_lt [lemma, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_eq [lemma, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_strorder [instance, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_equiv [instance, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.t [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt [module, in Coq.Structures.OrdersAlt]
OT_as_DT [module, in Coq.Structures.DecidableTypeEx]
OT_to_OrderTac.OTF [module, in Coq.Structures.OrdersTac]
OT_to_OrderTac [module, in Coq.Structures.OrdersTac]
OT_as_DT [module, in Coq.Structures.OrdersEx]
over [definition, in Coq.ssr.ssreflect]
O_witness [definition, in Coq.Logic.ConstructiveEpsilon]
O_S [lemma, in Coq.Init.Peano]
O_or_S [lemma, in Coq.Arith.Peano_dec]
| 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 | (22207 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 | (923 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 | (744 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 | (1482 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 | (500 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 | (10360 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 | (910 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 | (573 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 | (386 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 | (286 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 | (467 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 | (631 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 | (1123 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 | (3677 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 | (145 entries) |