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 (3098 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 (294 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 (28 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 (397 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 (9 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 (1414 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 (80 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 (7 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 (35 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 (35 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 (135 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 (84 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 (555 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 (25 entries)

L

last [definition, in Ssreflect.seq]
lastI [lemma, in Ssreflect.seq]
LastNil [constructor, in Ssreflect.seq]
lastP [lemma, in Ssreflect.seq]
LastRcons [constructor, in Ssreflect.seq]
last_map [lemma, in Ssreflect.seq]
last_nth [lemma, in Ssreflect.seq]
last_ind [lemma, in Ssreflect.seq]
last_spec [inductive, in Ssreflect.seq]
last_rcons [lemma, in Ssreflect.seq]
last_cat [lemma, in Ssreflect.seq]
last_cons [lemma, in Ssreflect.seq]
left_loop [definition, in Ssreflect.ssrfun]
left_commutative [definition, in Ssreflect.ssrfun]
left_id [definition, in Ssreflect.ssrfun]
left_distributive [definition, in Ssreflect.ssrfun]
left_zero [definition, in Ssreflect.ssrfun]
left_injective [definition, in Ssreflect.ssrfun]
left_inverse [definition, in Ssreflect.ssrfun]
left_transitive [definition, in Ssreflect.ssrbool]
leP [lemma, in Ssreflect.ssrnat]
leq [definition, in Ssreflect.ssrnat]
leqif [definition, in Ssreflect.ssrnat]
leqifP [lemma, in Ssreflect.ssrnat]
leqif_mul [lemma, in Ssreflect.ssrnat]
leqif_add [lemma, in Ssreflect.ssrnat]
leqif_eq [lemma, in Ssreflect.ssrnat]
leqif_geq [lemma, in Ssreflect.ssrnat]
leqif_trans [lemma, in Ssreflect.ssrnat]
leqif_refl [lemma, in Ssreflect.ssrnat]
leqNgt [lemma, in Ssreflect.ssrnat]
leqnn [lemma, in Ssreflect.ssrnat]
LeqNotGtn [constructor, in Ssreflect.ssrnat]
leqnSn [lemma, in Ssreflect.ssrnat]
leqn0 [lemma, in Ssreflect.ssrnat]
leqP [lemma, in Ssreflect.ssrnat]
leqSpred [lemma, in Ssreflect.ssrnat]
leqW [lemma, in Ssreflect.ssrnat]
leq_of_leqif [definition, in Ssreflect.ssrnat]
leq_sqr [lemma, in Ssreflect.ssrnat]
leq_Sdouble [lemma, in Ssreflect.ssrnat]
leq_double [lemma, in Ssreflect.ssrnat]
leq_b1 [lemma, in Ssreflect.ssrnat]
leq_exp2r [lemma, in Ssreflect.ssrnat]
leq_pexp2l [lemma, in Ssreflect.ssrnat]
leq_exp2l [lemma, in Ssreflect.ssrnat]
leq_pmul2r [lemma, in Ssreflect.ssrnat]
leq_pmul2l [lemma, in Ssreflect.ssrnat]
leq_mul [lemma, in Ssreflect.ssrnat]
leq_mul2r [lemma, in Ssreflect.ssrnat]
leq_mul2l [lemma, in Ssreflect.ssrnat]
leq_pmulr [lemma, in Ssreflect.ssrnat]
leq_pmull [lemma, in Ssreflect.ssrnat]
leq_min [lemma, in Ssreflect.ssrnat]
leq_maxr [lemma, in Ssreflect.ssrnat]
leq_maxl [lemma, in Ssreflect.ssrnat]
leq_max [lemma, in Ssreflect.ssrnat]
leq_sub [lemma, in Ssreflect.ssrnat]
leq_sub2l [lemma, in Ssreflect.ssrnat]
leq_sub2r [lemma, in Ssreflect.ssrnat]
leq_subr [lemma, in Ssreflect.ssrnat]
leq_subLR [lemma, in Ssreflect.ssrnat]
leq_addl [lemma, in Ssreflect.ssrnat]
leq_addr [lemma, in Ssreflect.ssrnat]
leq_add [lemma, in Ssreflect.ssrnat]
leq_add2r [lemma, in Ssreflect.ssrnat]
leq_add2l [lemma, in Ssreflect.ssrnat]
leq_xor_gtn [inductive, in Ssreflect.ssrnat]
leq_total [lemma, in Ssreflect.ssrnat]
leq_ltn_trans [lemma, in Ssreflect.ssrnat]
leq_trans [lemma, in Ssreflect.ssrnat]
leq_eqVlt [lemma, in Ssreflect.ssrnat]
leq_pred [lemma, in Ssreflect.ssrnat]
leq_size_perm [lemma, in Ssreflect.seq]
leq_size_uniq [lemma, in Ssreflect.seq]
leq_ord [lemma, in Ssreflect.fintype]
leq_bump2 [lemma, in Ssreflect.fintype]
leq_bump [lemma, in Ssreflect.fintype]
leq_image_card [lemma, in Ssreflect.fintype]
leq0n [lemma, in Ssreflect.ssrnat]
le_irrelevance [lemma, in Ssreflect.ssrnat]
lift [definition, in Ssreflect.fintype]
liftK [lemma, in Ssreflect.fintype]
lift_max [lemma, in Ssreflect.fintype]
lift_inj [lemma, in Ssreflect.fintype]
lift_subproof [lemma, in Ssreflect.fintype]
lift0 [lemma, in Ssreflect.fintype]
LocalGlobal [section, in Ssreflect.ssrbool]
LocalGlobal.allQ1 [variable, in Ssreflect.ssrbool]
LocalGlobal.allQ1l [variable, in Ssreflect.ssrbool]
LocalGlobal.allQ2 [variable, in Ssreflect.ssrbool]
LocalGlobal.d1 [variable, in Ssreflect.ssrbool]
LocalGlobal.D1 [variable, in Ssreflect.ssrbool]
LocalGlobal.d1' [variable, in Ssreflect.ssrbool]
LocalGlobal.d2 [variable, in Ssreflect.ssrbool]
LocalGlobal.D2 [variable, in Ssreflect.ssrbool]
LocalGlobal.d2' [variable, in Ssreflect.ssrbool]
LocalGlobal.d3 [variable, in Ssreflect.ssrbool]
LocalGlobal.D3 [variable, in Ssreflect.ssrbool]
LocalGlobal.d3' [variable, in Ssreflect.ssrbool]
LocalGlobal.f [variable, in Ssreflect.ssrbool]
LocalGlobal.f' [variable, in Ssreflect.ssrbool]
LocalGlobal.g [variable, in Ssreflect.ssrbool]
LocalGlobal.h [variable, in Ssreflect.ssrbool]
LocalGlobal.P1 [variable, in Ssreflect.ssrbool]
LocalGlobal.P2 [variable, in Ssreflect.ssrbool]
LocalGlobal.P3 [variable, in Ssreflect.ssrbool]
LocalGlobal.Q1 [variable, in Ssreflect.ssrbool]
LocalGlobal.Q1l [variable, in Ssreflect.ssrbool]
LocalGlobal.Q2 [variable, in Ssreflect.ssrbool]
LocalGlobal.sub1 [variable, in Ssreflect.ssrbool]
LocalGlobal.sub2 [variable, in Ssreflect.ssrbool]
LocalGlobal.sub3 [variable, in Ssreflect.ssrbool]
LocalGlobal.T1 [variable, in Ssreflect.ssrbool]
LocalGlobal.T2 [variable, in Ssreflect.ssrbool]
LocalGlobal.T3 [variable, in Ssreflect.ssrbool]
LocalProperties [section, in Ssreflect.ssrbool]
LocalProperties.d1 [variable, in Ssreflect.ssrbool]
LocalProperties.d2 [variable, in Ssreflect.ssrbool]
LocalProperties.d3 [variable, in Ssreflect.ssrbool]
LocalProperties.f [variable, in Ssreflect.ssrbool]
LocalProperties.T1 [variable, in Ssreflect.ssrbool]
LocalProperties.T2 [variable, in Ssreflect.ssrbool]
LocalProperties.T3 [variable, in Ssreflect.ssrbool]
lock [lemma, in Ssreflect.ssreflect]
locked [definition, in Ssreflect.ssreflect]
locked_with_unlockable [definition, in Ssreflect.ssreflect]
locked_withE [lemma, in Ssreflect.ssreflect]
locked_with [definition, in Ssreflect.ssreflect]
lshift [definition, in Ssreflect.fintype]
lshift_subproof [lemma, in Ssreflect.fintype]
ltn [definition, in Ssreflect.ssrnat]
ltngtP [lemma, in Ssreflect.ssrnat]
ltnn [lemma, in Ssreflect.ssrnat]
ltnNge [lemma, in Ssreflect.ssrnat]
LtnNotGeq [constructor, in Ssreflect.ssrnat]
ltnP [lemma, in Ssreflect.ssrnat]
ltnS [lemma, in Ssreflect.ssrnat]
ltnSn [lemma, in Ssreflect.ssrnat]
ltnW [lemma, in Ssreflect.ssrnat]
ltn_leqif [lemma, in Ssreflect.ssrnat]
ltn_sqr [lemma, in Ssreflect.ssrnat]
ltn_Sdouble [lemma, in Ssreflect.ssrnat]
ltn_double [lemma, in Ssreflect.ssrnat]
ltn_exp2r [lemma, in Ssreflect.ssrnat]
ltn_pexp2l [lemma, in Ssreflect.ssrnat]
ltn_exp2l [lemma, in Ssreflect.ssrnat]
ltn_expl [lemma, in Ssreflect.ssrnat]
ltn_mul [lemma, in Ssreflect.ssrnat]
ltn_Pmulr [lemma, in Ssreflect.ssrnat]
ltn_Pmull [lemma, in Ssreflect.ssrnat]
ltn_pmul2r [lemma, in Ssreflect.ssrnat]
ltn_pmul2l [lemma, in Ssreflect.ssrnat]
ltn_mul2r [lemma, in Ssreflect.ssrnat]
ltn_mul2l [lemma, in Ssreflect.ssrnat]
ltn_subRL [lemma, in Ssreflect.ssrnat]
ltn_sub2l [lemma, in Ssreflect.ssrnat]
ltn_sub2r [lemma, in Ssreflect.ssrnat]
ltn_addl [lemma, in Ssreflect.ssrnat]
ltn_addr [lemma, in Ssreflect.ssrnat]
ltn_add2r [lemma, in Ssreflect.ssrnat]
ltn_add2l [lemma, in Ssreflect.ssrnat]
ltn_xor_geq [inductive, in Ssreflect.ssrnat]
ltn_trans [lemma, in Ssreflect.ssrnat]
ltn_neqAle [lemma, in Ssreflect.ssrnat]
ltn_eqF [lemma, in Ssreflect.ssrnat]
ltn_predK [lemma, in Ssreflect.ssrnat]
ltn_size_undup [lemma, in Ssreflect.seq]
ltn_unsplit [lemma, in Ssreflect.fintype]
ltn_ord [lemma, in Ssreflect.fintype]
ltn0 [lemma, in Ssreflect.ssrnat]
ltn0Sn [lemma, in Ssreflect.ssrnat]
ltP [lemma, in Ssreflect.ssrnat]
lt_irrelevance [lemma, in Ssreflect.ssrnat]
lt0b [lemma, in Ssreflect.ssrnat]
lt0n [lemma, in Ssreflect.ssrnat]
lt0n_neq0 [lemma, in Ssreflect.ssrnat]



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 (3098 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 (294 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 (28 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 (397 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 (9 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 (1414 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 (80 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 (7 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 (35 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 (35 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 (135 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 (84 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 (555 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 (25 entries)