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 | (21799 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 | (910 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 | (727 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 | (494 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 | (10179 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 | (676 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 | (287 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 | (1332 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 | (3609 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) |

## L

L [definition, in Coq.Vectors.Fin]land [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

land [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

land [definition, in Coq.Init.Nat]

land_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

land31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

last [definition, in Coq.Vectors.VectorDef]

last [definition, in Coq.Lists.List]

law_cosines [lemma, in Coq.Reals.Rgeom]

lb_to_glb [lemma, in Coq.Reals.SeqProp]

ldiff [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

ldiff [definition, in Coq.Init.Nat]

ldiff_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

ldiff31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

le [inductive, in Coq.Init.Peano]

Le [library]

Leaf [constructor, in Coq.micromega.VarMap]

leaf [definition, in Coq.micromega.ZMicromega]

leA_Tree_Node [lemma, in Coq.Sorting.Heap]

leA_Tree_Leaf [lemma, in Coq.Sorting.Heap]

leA_Tree [definition, in Coq.Sorting.Heap]

leb [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

leb [definition, in Coq.Init.Nat]

leb [definition, in Coq.Bool.Bool]

leb [abbreviation, in Coq.Arith.Compare_dec]

LebIsTotal [module, in Coq.Structures.Orders]

LebIsTotal.leb_total [axiom, in Coq.Structures.Orders]

LebIsTransitive [module, in Coq.Structures.Orders]

LebIsTransitive.leb_trans [axiom, in Coq.Structures.Orders]

LebNotation [module, in Coq.Structures.Orders]

_ <=? _ [notation, in Coq.Structures.Orders]

LeBool [module, in Coq.Structures.Orders]

LeBool' [module, in Coq.Structures.Orders]

LebSpec [module, in Coq.Structures.Orders]

LebSpec.leb_le [axiom, in Coq.Structures.Orders]

leb_le [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

leb_refl [lemma, in Coq.Sets.Uniset]

leb_implb [lemma, in Coq.Bool.Bool]

leb_compare [lemma, in Coq.Arith.Compare_dec]

leb_complete_conv [lemma, in Coq.Arith.Compare_dec]

leb_correct_conv [lemma, in Coq.Arith.Compare_dec]

leb_complete [lemma, in Coq.Arith.Compare_dec]

leb_correct [lemma, in Coq.Arith.Compare_dec]

leb_iff_conv [lemma, in Coq.Arith.Compare_dec]

leb_iff [abbreviation, in Coq.Arith.Compare_dec]

left [constructor, in Coq.Init.Specif]

left [abbreviation, in Coq.setoid_ring.Field_theory]

leftinv_is_rightinv_interv [lemma, in Coq.Reals.Ranalysis5]

leftinv_is_rightinv [lemma, in Coq.Reals.Ranalysis5]

left_transitive [definition, in Coq.ssr.ssrbool]

Left_idx [constructor, in Coq.quote.Quote]

left_loop [definition, in Coq.ssr.ssrfun]

left_commutative [definition, in Coq.ssr.ssrfun]

left_id [definition, in Coq.ssr.ssrfun]

left_distributive [definition, in Coq.ssr.ssrfun]

left_zero [definition, in Coq.ssr.ssrfun]

left_injective [definition, in Coq.ssr.ssrfun]

left_inverse [definition, in Coq.ssr.ssrfun]

left_sym [constructor, in Coq.Relations.Relation_Operators]

left_lex [constructor, in Coq.Relations.Relation_Operators]

left_prefix [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]

LeIsLtEq [module, in Coq.Structures.Orders]

LeIsLtEq.le_lteq [axiom, in Coq.Structures.Orders]

lel [definition, in Coq.Lists.List]

lelistA [abbreviation, in Coq.Sorting.Sorted]

lelistA_inv [abbreviation, in Coq.Sorting.Sorted]

lel_nil [lemma, in Coq.Lists.List]

lel_tail [lemma, in Coq.Lists.List]

lel_cons [lemma, in Coq.Lists.List]

lel_cons_cons [lemma, in Coq.Lists.List]

lel_trans [lemma, in Coq.Lists.List]

lel_refl [lemma, in Coq.Lists.List]

Lemma1 [lemma, in Coq.Sets.Relations_2_facts]

length [definition, in Coq.Init.Datatypes]

length [definition, in Coq.Strings.String]

length [abbreviation, in Coq.Lists.List]

length_map [lemma, in Coq.rtauto.Bintree]

length_order.n [variable, in Coq.Lists.List]

length_order.m [variable, in Coq.Lists.List]

length_order.l [variable, in Coq.Lists.List]

length_order.b [variable, in Coq.Lists.List]

length_order.a [variable, in Coq.Lists.List]

length_order.A [variable, in Coq.Lists.List]

length_order [section, in Coq.Lists.List]

length_zero_iff_nil [lemma, in Coq.Lists.List]

LeNotation [module, in Coq.Structures.Orders]

_ <= _ <= _ [notation, in Coq.Structures.Orders]

_ >= _ [notation, in Coq.Structures.Orders]

_ <= _ [notation, in Coq.Structures.Orders]

less_than_empty [lemma, in Coq.Sets.Powerset_facts]

less_than_singleton [lemma, in Coq.Sets.Powerset_Classical_facts]

Lexicographic_Exponentiation.List [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Exponentiation.Nil [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Exponentiation.leA [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Exponentiation.A [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Exponentiation [section, in Coq.Relations.Relation_Operators]

Lexicographic_Product.leB [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Product.leA [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Product.B [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Product.A [variable, in Coq.Relations.Relation_Operators]

Lexicographic_Product [section, in Coq.Relations.Relation_Operators]

Lexicographic_Exponentiation [library]

Lexicographic_Product [library]

LexProd [abbreviation, in Coq.Wellfounded.Lexicographic_Product]

lexprod [inductive, in Coq.Relations.Relation_Operators]

lex_exp [definition, in Coq.Relations.Relation_Operators]

Lex_Exp [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]

le_minus [abbreviation, in Coq.Arith.Minus]

le_plus_minus [lemma, in Coq.Arith.Minus]

le_plus_minus_r [lemma, in Coq.Arith.Minus]

le_n_2n [lemma, in Coq.Reals.Rprod]

le_O_IZR [abbreviation, in Coq.Reals.RIneq]

le_epsilon [lemma, in Coq.Reals.RIneq]

le_IZR_R1 [lemma, in Coq.Reals.RIneq]

le_IZR [lemma, in Coq.Reals.RIneq]

le_0_IZR [lemma, in Coq.Reals.RIneq]

le_INR [lemma, in Coq.Reals.RIneq]

le_n_O_eq [abbreviation, in Coq.Arith.Le]

le_Sn_O [abbreviation, in Coq.Arith.Le]

le_O_n [abbreviation, in Coq.Arith.Le]

le_elim_rel [lemma, in Coq.Arith.Le]

le_pred [abbreviation, in Coq.Arith.Le]

le_pred_n [abbreviation, in Coq.Arith.Le]

le_Sn_le [lemma, in Coq.Arith.Le]

le_Sn_n [abbreviation, in Coq.Arith.Le]

le_n_Sn [abbreviation, in Coq.Arith.Le]

le_S_n [lemma, in Coq.Arith.Le]

le_n_S [lemma, in Coq.Arith.Le]

le_n_0_eq [lemma, in Coq.Arith.Le]

le_Sn_0 [abbreviation, in Coq.Arith.Le]

le_0_n [abbreviation, in Coq.Arith.Le]

le_antisym [abbreviation, in Coq.Arith.Le]

le_trans [abbreviation, in Coq.Arith.Le]

le_refl [abbreviation, in Coq.Arith.Le]

le_gt_trans [lemma, in Coq.Arith.Gt]

le_gt_S [lemma, in Coq.Arith.Gt]

le_S_gt [lemma, in Coq.Arith.Gt]

le_not_gt [lemma, in Coq.Arith.Gt]

Le_AsB [abbreviation, in Coq.Wellfounded.Disjoint_Union]

le_max_r [definition, in Coq.Arith.Max]

le_max_l [definition, in Coq.Arith.Max]

le_le_S_eq [lemma, in Coq.Arith.Compare]

le_decide [lemma, in Coq.Arith.Compare]

le_dec [lemma, in Coq.Arith.Compare]

le_or_le_S [definition, in Coq.Arith.Compare]

le_total_order [lemma, in Coq.Sets.Integers]

le_Order [lemma, in Coq.Sets.Integers]

le_trans [lemma, in Coq.Sets.Integers]

le_antisym [lemma, in Coq.Sets.Integers]

le_reflexive [lemma, in Coq.Sets.Integers]

le_sup [constructor, in Coq.Wellfounded.Well_Ordering]

le_WO [inductive, in Coq.Wellfounded.Well_Ordering]

le_ni_le [lemma, in Coq.NArith.Ndist]

le_plus_trans [lemma, in Coq.Arith.Plus]

le_plus_r [lemma, in Coq.Arith.Plus]

le_plus_l [lemma, in Coq.Arith.Plus]

le_n_S [lemma, in Coq.Init.Peano]

le_0_n [lemma, in Coq.Init.Peano]

le_S_n [lemma, in Coq.Init.Peano]

le_pred [lemma, in Coq.Init.Peano]

le_S [constructor, in Coq.Init.Peano]

le_n [constructor, in Coq.Init.Peano]

le_min_r [definition, in Coq.Arith.Min]

le_min_l [definition, in Coq.Arith.Min]

le_double [lemma, in Coq.Reals.ArithProp]

le_minusni_n [lemma, in Coq.Reals.ArithProp]

le_bb [constructor, in Coq.Relations.Relation_Operators]

le_ab [constructor, in Coq.Relations.Relation_Operators]

le_aa [constructor, in Coq.Relations.Relation_Operators]

le_AsB [inductive, in Coq.Relations.Relation_Operators]

le_lt_SS [lemma, in Coq.funind.Recdef]

le_unique [lemma, in Coq.Arith.Peano_dec]

le_or_lt [abbreviation, in Coq.Arith.Lt]

le_lt_or_eq [lemma, in Coq.Arith.Lt]

le_lt_or_eq_iff [abbreviation, in Coq.Arith.Lt]

le_lt_trans [abbreviation, in Coq.Arith.Lt]

le_not_lt [lemma, in Coq.Arith.Lt]

le_lt_n_Sm [lemma, in Coq.Arith.Lt]

le_Pmult_nat [lemma, in Coq.PArith.Pnat]

le_dec [lemma, in Coq.Arith.Compare_dec]

le_lt_eq_dec [definition, in Coq.Arith.Compare_dec]

le_gt_dec [definition, in Coq.Arith.Compare_dec]

le_ge_dec [definition, in Coq.Arith.Compare_dec]

le_le_S_dec [definition, in Coq.Arith.Compare_dec]

le_lt_dec [definition, in Coq.Arith.Compare_dec]

Lget [definition, in Coq.rtauto.Bintree]

Lget_app_Some [lemma, in Coq.rtauto.Bintree]

Lget_app [lemma, in Coq.rtauto.Bintree]

Lget_map [lemma, in Coq.rtauto.Bintree]

Lia [library]

limit_inv [lemma, in Coq.Reals.Rlimit]

limit_comp [lemma, in Coq.Reals.Rlimit]

limit_mul [lemma, in Coq.Reals.Rlimit]

limit_free [lemma, in Coq.Reals.Rlimit]

limit_minus [lemma, in Coq.Reals.Rlimit]

limit_Ropp [lemma, in Coq.Reals.Rlimit]

limit_plus [lemma, in Coq.Reals.Rlimit]

limit_in [definition, in Coq.Reals.Rlimit]

limit1_in [definition, in Coq.Reals.Rlimit]

limit1_imp [lemma, in Coq.Reals.Rpower]

limit1_ext [lemma, in Coq.Reals.Rpower]

lim_x [lemma, in Coq.Reals.Rlimit]

linear [inductive, in Coq.btauto.Algebra]

linear [record, in Coq.setoid_ring.Field_theory]

linear_reduce [lemma, in Coq.btauto.Algebra]

linear_reduce_aux [lemma, in Coq.btauto.Algebra]

linear_valid_incl [lemma, in Coq.btauto.Algebra]

linear_le_compat [lemma, in Coq.btauto.Algebra]

linear_poly [constructor, in Coq.btauto.Algebra]

linear_cst [constructor, in Coq.btauto.Algebra]

linear_search [definition, in Coq.Logic.ConstructiveEpsilon]

list [inductive, in Coq.Init.Datatypes]

list [abbreviation, in Coq.Lists.List]

List [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]

List [library]

ListDec [library]

Listing [definition, in Coq.Logic.FinFun]

ListNotations [module, in Coq.Lists.List]

[ _ ; _ ; .. ; _ ] (list_scope) [notation, in Coq.Lists.List]

[ _ ] (list_scope) [notation, in Coq.Lists.List]

[ ] (list_scope) [notation, in Coq.Lists.List]

ListOps [section, in Coq.Lists.List]

ListOps.A [variable, in Coq.Lists.List]

ListOps.eq_dec [variable, in Coq.Lists.List]

ListOps.Reverse_Induction [section, in Coq.Lists.List]

ListPairs [section, in Coq.Lists.List]

ListPairs.A [variable, in Coq.Lists.List]

ListPairs.B [variable, in Coq.Lists.List]

Lists [section, in Coq.Lists.List]

ListSet [library]

Lists.A [variable, in Coq.Lists.List]

ListTactics [library]

list_nth [definition, in Coq.btauto.Algebra]

list_reifyl [definition, in Coq.setoid_ring.Ncring_tac]

list_contents [abbreviation, in Coq.Sorting.PermutEq]

list_contents_app [lemma, in Coq.Sorting.PermutSetoid]

list_contents [definition, in Coq.Sorting.PermutSetoid]

list_replace_nth_2 [lemma, in Coq.btauto.Reflect]

list_replace_nth_1 [lemma, in Coq.btauto.Reflect]

list_nth_nil [lemma, in Coq.btauto.Reflect]

list_nth_succ [lemma, in Coq.btauto.Reflect]

list_nth_base [lemma, in Coq.btauto.Reflect]

list_replace [definition, in Coq.btauto.Reflect]

list_to_heap [lemma, in Coq.Sorting.Heap]

list_ind [abbreviation, in Coq.Lists.List]

list_rec [abbreviation, in Coq.Lists.List]

list_rect [abbreviation, in Coq.Lists.List]

list_prod [definition, in Coq.Lists.List]

list_power [definition, in Coq.Lists.List]

list_eq_dec [lemma, in Coq.Lists.List]

list_eqdec [instance, in Coq.Classes.EquivDec]

Little [module, in Coq.Init.Decimal]

Little.double [definition, in Coq.Init.Decimal]

Little.succ [definition, in Coq.Init.Decimal]

Little.succ_double [definition, in Coq.Init.Decimal]

ln [definition, in Coq.Reals.Rpower]

lnorm [definition, in Coq.Numbers.DecimalFacts]

lnot31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

ln_lt_2 [lemma, in Coq.Reals.Rpower]

ln_continue [lemma, in Coq.Reals.Rpower]

ln_Rinv [lemma, in Coq.Reals.Rpower]

ln_mult [lemma, in Coq.Reals.Rpower]

ln_inv [lemma, in Coq.Reals.Rpower]

ln_lt_inv [lemma, in Coq.Reals.Rpower]

ln_1 [lemma, in Coq.Reals.Rpower]

ln_exp [lemma, in Coq.Reals.Rpower]

ln_increasing [lemma, in Coq.Reals.Rpower]

ln_exists [lemma, in Coq.Reals.Rpower]

ln_exists1 [lemma, in Coq.Reals.Rpower]

LocalGlobal [section, in Coq.ssr.ssrbool]

LocalGlobal.allQ1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.allQ1l [variable, in Coq.ssr.ssrbool]

LocalGlobal.allQ2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.d1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.D1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.d1' [variable, in Coq.ssr.ssrbool]

LocalGlobal.d2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.D2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.d2' [variable, in Coq.ssr.ssrbool]

LocalGlobal.d3 [variable, in Coq.ssr.ssrbool]

LocalGlobal.D3 [variable, in Coq.ssr.ssrbool]

LocalGlobal.d3' [variable, in Coq.ssr.ssrbool]

LocalGlobal.f [variable, in Coq.ssr.ssrbool]

LocalGlobal.f' [variable, in Coq.ssr.ssrbool]

LocalGlobal.g [variable, in Coq.ssr.ssrbool]

LocalGlobal.h [variable, in Coq.ssr.ssrbool]

LocalGlobal.P1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.P2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.P3 [variable, in Coq.ssr.ssrbool]

LocalGlobal.Q1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.Q1l [variable, in Coq.ssr.ssrbool]

LocalGlobal.Q2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.sub1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.sub2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.sub3 [variable, in Coq.ssr.ssrbool]

LocalGlobal.T1 [variable, in Coq.ssr.ssrbool]

LocalGlobal.T2 [variable, in Coq.ssr.ssrbool]

LocalGlobal.T3 [variable, in Coq.ssr.ssrbool]

LocallySorted [inductive, in Coq.Sorting.Sorted]

Locally_confluent [definition, in Coq.Sets.Relations_3]

locally_confluent [definition, in Coq.Sets.Relations_3]

LocalProperties [section, in Coq.ssr.ssrbool]

LocalProperties.d1 [variable, in Coq.ssr.ssrbool]

LocalProperties.d2 [variable, in Coq.ssr.ssrbool]

LocalProperties.d3 [variable, in Coq.ssr.ssrbool]

LocalProperties.f [variable, in Coq.ssr.ssrbool]

LocalProperties.T1 [variable, in Coq.ssr.ssrbool]

LocalProperties.T2 [variable, in Coq.ssr.ssrbool]

LocalProperties.T3 [variable, in Coq.ssr.ssrbool]

local_mkpow_ok [lemma, in Coq.setoid_ring.Ring_polynom]

lock [lemma, in Coq.ssr.ssreflect]

locked [definition, in Coq.ssr.ssreflect]

locked_withE [lemma, in Coq.ssr.ssreflect]

locked_with [definition, in Coq.ssr.ssreflect]

Logic [library]

Logic_lemmas.equality.z [variable, in Coq.Init.Logic]

Logic_lemmas.equality.y [variable, in Coq.Init.Logic]

Logic_lemmas.equality.x [variable, in Coq.Init.Logic]

Logic_lemmas.equality.f [variable, in Coq.Init.Logic]

Logic_lemmas.equality.B [variable, in Coq.Init.Logic]

Logic_lemmas.equality.A [variable, in Coq.Init.Logic]

Logic_lemmas.equality [section, in Coq.Init.Logic]

Logic_lemmas [section, in Coq.Init.Logic]

Logic_Type [library]

log_sup_shift_nat [lemma, in Coq.ZArith.Zlogarithm]

log_inf_shift_nat [lemma, in Coq.ZArith.Zlogarithm]

log_near_correct2 [lemma, in Coq.ZArith.Zlogarithm]

log_near_correct1 [lemma, in Coq.ZArith.Zlogarithm]

log_near [definition, in Coq.ZArith.Zlogarithm]

log_sup_le_Slog_inf [lemma, in Coq.ZArith.Zlogarithm]

log_inf_le_log_sup [lemma, in Coq.ZArith.Zlogarithm]

log_sup_correct2 [lemma, in Coq.ZArith.Zlogarithm]

log_sup_log_inf [lemma, in Coq.ZArith.Zlogarithm]

log_sup_correct1 [lemma, in Coq.ZArith.Zlogarithm]

log_inf_correct2 [definition, in Coq.ZArith.Zlogarithm]

log_inf_correct1 [definition, in Coq.ZArith.Zlogarithm]

log_inf_correct [lemma, in Coq.ZArith.Zlogarithm]

log_sup [definition, in Coq.ZArith.Zlogarithm]

log_inf [definition, in Coq.ZArith.Zlogarithm]

Log_pos [section, in Coq.ZArith.Zlogarithm]

log_inf_bounded [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

log2 [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

log2 [definition, in Coq.Init.Nat]

Log2 [module, in Coq.Numbers.NatInt.NZLog]

log2_nonpos [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

log2_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

log2_iter_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

log2_iter [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

log2_phi_bounded [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

log2_iter [definition, in Coq.Init.Nat]

Log2.log2 [axiom, in Coq.Numbers.NatInt.NZLog]

lor [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

lor [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

lor [definition, in Coq.Init.Nat]

lor_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

lor31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

Lower_Bound_definition [constructor, in Coq.Sets.Cpo]

Lower_Bound [inductive, in Coq.Sets.Cpo]

low_trans [lemma, in Coq.Sorting.Heap]

Lqa [library]

Lra [library]

lshiftl [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]

LSorted_consn [constructor, in Coq.Sorting.Sorted]

LSorted_cons1 [constructor, in Coq.Sorting.Sorted]

LSorted_nil [constructor, in Coq.Sorting.Sorted]

LT [constructor, in Coq.Structures.OrderedType]

lt [definition, in Coq.Init.Peano]

Lt [constructor, in Coq.Init.Datatypes]

Lt [library]

Ltac [library]

ltb [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

ltb [definition, in Coq.Init.Nat]

LtbNotation [module, in Coq.Structures.Orders]

_ [notation, in Coq.Structures.Orders]

LtBool [module, in Coq.Structures.Orders]

LtBool' [module, in Coq.Structures.Orders]

LtbSpec [module, in Coq.Structures.Orders]

LtbSpec.ltb_lt [axiom, in Coq.Structures.Orders]

ltb_lt [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

LtIsTotal [module, in Coq.Structures.Orders]

LtIsTotal.lt_total [axiom, in Coq.Structures.Orders]

Ltl [inductive, in Coq.Relations.Relation_Operators]

ltl [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]

LtLeNotation [module, in Coq.Structures.Orders]

_ < _ <= _ [notation, in Coq.Structures.Orders]

_ <= _ < _ [notation, in Coq.Structures.Orders]

ltl_unit [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]

LtNotation [module, in Coq.Structures.Orders]

_ < _ < _ [notation, in Coq.Structures.Orders]

_ > _ [notation, in Coq.Structures.Orders]

_ < _ [notation, in Coq.Structures.Orders]

ltof [definition, in Coq.Arith.Wf_nat]

lt_O_minus_lt [lemma, in Coq.Arith.Minus]

lt_minus [abbreviation, in Coq.Arith.Minus]

LT_WF_REL.F_compat [variable, in Coq.Arith.Wf_nat]

LT_WF_REL.F [variable, in Coq.Arith.Wf_nat]

LT_WF_REL.R [variable, in Coq.Arith.Wf_nat]

LT_WF_REL.A [variable, in Coq.Arith.Wf_nat]

LT_WF_REL [section, in Coq.Arith.Wf_nat]

lt_wf_double_ind [lemma, in Coq.Arith.Wf_nat]

lt_wf_double_rec [lemma, in Coq.Arith.Wf_nat]

lt_wf_ind [lemma, in Coq.Arith.Wf_nat]

lt_wf_rec [lemma, in Coq.Arith.Wf_nat]

lt_wf_rec1 [lemma, in Coq.Arith.Wf_nat]

lt_wf [lemma, in Coq.Arith.Wf_nat]

lt_O_IZR [abbreviation, in Coq.Reals.RIneq]

lt_INR_0 [abbreviation, in Coq.Reals.RIneq]

lt_IZR [lemma, in Coq.Reals.RIneq]

lt_0_IZR [lemma, in Coq.Reals.RIneq]

lt_1_INR [lemma, in Coq.Reals.RIneq]

lt_INR [lemma, in Coq.Reals.RIneq]

lt_0_INR [lemma, in Coq.Reals.RIneq]

lt_or_eq [definition, in Coq.Arith.Compare]

lt_div2 [lemma, in Coq.Arith.Div2]

lt_plus_trans [lemma, in Coq.Arith.Plus]

lt_ge_dec [definition, in Coq.Arith.Bool_nat]

lt_minus_O_lt [lemma, in Coq.Reals.ArithProp]

Lt_tl [constructor, in Coq.Relations.Relation_Operators]

Lt_hd [constructor, in Coq.Relations.Relation_Operators]

Lt_nil [constructor, in Coq.Relations.Relation_Operators]

lt_O_fact [lemma, in Coq.Arith.Factorial]

lt_n_O [abbreviation, in Coq.Arith.Lt]

lt_O_neq [abbreviation, in Coq.Arith.Lt]

lt_O_Sn [abbreviation, in Coq.Arith.Lt]

lt_le_weak [abbreviation, in Coq.Arith.Lt]

lt_le_trans [abbreviation, in Coq.Arith.Lt]

lt_trans [abbreviation, in Coq.Arith.Lt]

lt_pred_n_n [lemma, in Coq.Arith.Lt]

lt_pred [lemma, in Coq.Arith.Lt]

lt_S_n [lemma, in Coq.Arith.Lt]

lt_n_S [lemma, in Coq.Arith.Lt]

lt_S [abbreviation, in Coq.Arith.Lt]

lt_n_Sn [abbreviation, in Coq.Arith.Lt]

lt_0_neq [lemma, in Coq.Arith.Lt]

lt_n_0 [abbreviation, in Coq.Arith.Lt]

lt_0_Sn [abbreviation, in Coq.Arith.Lt]

lt_asym [abbreviation, in Coq.Arith.Lt]

lt_not_le [lemma, in Coq.Arith.Lt]

lt_n_Sm_le [lemma, in Coq.Arith.Lt]

lt_le_S [lemma, in Coq.Arith.Lt]

lt_irrefl [abbreviation, in Coq.Arith.Lt]

lt_O_nat_of_P [abbreviation, in Coq.PArith.Pnat]

lt_dec [lemma, in Coq.Arith.Compare_dec]

lt_eq_lt_dec [definition, in Coq.Arith.Compare_dec]

lub [definition, in Coq.Reals.SeqProp]

Lub [inductive, in Coq.Sets.Cpo]

Lub_definition [constructor, in Coq.Sets.Cpo]

lxor [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

lxor [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]

lxor [definition, in Coq.Init.Nat]

lxor_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]

lxor31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]

L_R [definition, in Coq.Vectors.Fin]

L_sanity [lemma, in Coq.Vectors.Fin]

L1 [lemma, in Coq.Logic.Berardi]

l2i [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]

l2i_i2l [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]

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 | (21799 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 | (910 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 | (727 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 | (494 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 | (10179 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 | (676 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 | (287 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 | (1332 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 | (3609 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) |