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)

O

oapp [abbreviation, in Ssreflect.ssrfun]
obind [abbreviation, in Ssreflect.ssrfun]
ocancel [definition, in Ssreflect.ssrfun]
odd [definition, in Ssreflect.ssrnat]
oddb [lemma, in Ssreflect.ssrnat]
odd_gt2 [lemma, in Ssreflect.ssrnat]
odd_gt0 [lemma, in Ssreflect.ssrnat]
odd_ltn [lemma, in Ssreflect.ssrnat]
odd_geq [lemma, in Ssreflect.ssrnat]
odd_double_half [lemma, in Ssreflect.ssrnat]
odd_double [lemma, in Ssreflect.ssrnat]
odd_exp [lemma, in Ssreflect.ssrnat]
odd_mul [lemma, in Ssreflect.ssrnat]
odd_opp [lemma, in Ssreflect.ssrnat]
odd_sub [lemma, in Ssreflect.ssrnat]
odd_add [lemma, in Ssreflect.ssrnat]
odflt [abbreviation, in Ssreflect.ssrfun]
ohead [definition, in Ssreflect.seq]
omap [abbreviation, in Ssreflect.ssrfun]
onPhantom [definition, in Ssreflect.ssrbool]
onT_bij [lemma, in Ssreflect.ssrbool]
onW_bij [lemma, in Ssreflect.ssrbool]
on_can_inj [lemma, in Ssreflect.ssrbool]
on1lT [lemma, in Ssreflect.ssrbool]
on1lW [lemma, in Ssreflect.ssrbool]
on1T [lemma, in Ssreflect.ssrbool]
on1W [lemma, in Ssreflect.ssrbool]
on2T [lemma, in Ssreflect.ssrbool]
on2W [lemma, in Ssreflect.ssrbool]
opair_of_sumK [lemma, in Ssreflect.choice]
opair_of_sum [definition, in Ssreflect.choice]
OperationProperties [section, in Ssreflect.ssrfun]
OperationProperties.R [variable, in Ssreflect.ssrfun]
OperationProperties.S [variable, in Ssreflect.ssrfun]
OperationProperties.SopSisS [section, in Ssreflect.ssrfun]
OperationProperties.SopSisT [section, in Ssreflect.ssrfun]
OperationProperties.SopTisR [section, in Ssreflect.ssrfun]
OperationProperties.SopTisS [section, in Ssreflect.ssrfun]
OperationProperties.SopTisT [section, in Ssreflect.ssrfun]
OperationProperties.T [variable, in Ssreflect.ssrfun]
OpsTheory [section, in Ssreflect.fintype]
OpsTheory.EnumPick [section, in Ssreflect.fintype]
OpsTheory.EnumPick.P [variable, in Ssreflect.fintype]
OpsTheory.T [variable, in Ssreflect.fintype]
Option [module, in Ssreflect.ssrfun]
OptionEqType [section, in Ssreflect.eqtype]
OptionEqType.T [variable, in Ssreflect.eqtype]
OptionFinType [section, in Ssreflect.fintype]
OptionFinType.T [variable, in Ssreflect.fintype]
option_countType [definition, in Ssreflect.choice]
option_countMixin [definition, in Ssreflect.choice]
option_choiceType [definition, in Ssreflect.choice]
option_choiceMixin [definition, in Ssreflect.choice]
option_eqType [definition, in Ssreflect.eqtype]
option_eqMixin [definition, in Ssreflect.eqtype]
option_finType [definition, in Ssreflect.fintype]
option_finMixin [definition, in Ssreflect.fintype]
option_enumP [lemma, in Ssreflect.fintype]
option_enum [definition, in Ssreflect.fintype]
Option.apply [definition, in Ssreflect.ssrfun]
Option.bind [definition, in Ssreflect.ssrfun]
Option.default [definition, in Ssreflect.ssrfun]
Option.map [definition, in Ssreflect.ssrfun]
opt_eqP [lemma, in Ssreflect.eqtype]
opt_eq [definition, in Ssreflect.eqtype]
orbA [lemma, in Ssreflect.ssrbool]
orbAC [lemma, in Ssreflect.ssrbool]
orbACA [lemma, in Ssreflect.ssrbool]
orbb [lemma, in Ssreflect.ssrbool]
orbC [lemma, in Ssreflect.ssrbool]
orbCA [lemma, in Ssreflect.ssrbool]
orbF [lemma, in Ssreflect.ssrbool]
orbK [lemma, in Ssreflect.ssrbool]
orbN [lemma, in Ssreflect.ssrbool]
orbT [lemma, in Ssreflect.ssrbool]
orb_id2r [lemma, in Ssreflect.ssrbool]
orb_id2l [lemma, in Ssreflect.ssrbool]
orb_idr [lemma, in Ssreflect.ssrbool]
orb_idl [lemma, in Ssreflect.ssrbool]
orb_andr [lemma, in Ssreflect.ssrbool]
orb_andl [lemma, in Ssreflect.ssrbool]
Ordinal [constructor, in Ssreflect.fintype]
ordinal [inductive, in Ssreflect.fintype]
OrdinalEnum [section, in Ssreflect.fintype]
OrdinalEnum.n [variable, in Ssreflect.fintype]
OrdinalPos [section, in Ssreflect.fintype]
OrdinalPos.n' [variable, in Ssreflect.fintype]
OrdinalSub [section, in Ssreflect.fintype]
OrdinalSub.n [variable, in Ssreflect.fintype]
ordinal_subFinType [definition, in Ssreflect.fintype]
ordinal_finType [definition, in Ssreflect.fintype]
ordinal_finMixin [definition, in Ssreflect.fintype]
ordinal_subCountType [definition, in Ssreflect.fintype]
ordinal_countType [definition, in Ssreflect.fintype]
ordinal_countMixin [definition, in Ssreflect.fintype]
ordinal_choiceType [definition, in Ssreflect.fintype]
ordinal_choiceMixin [definition, in Ssreflect.fintype]
ordinal_eqType [definition, in Ssreflect.fintype]
ordinal_eqMixin [definition, in Ssreflect.fintype]
ordinal_subType [definition, in Ssreflect.fintype]
ord_max [definition, in Ssreflect.fintype]
ord_enum_uniq [lemma, in Ssreflect.fintype]
ord_enum [definition, in Ssreflect.fintype]
ord_inj [lemma, in Ssreflect.fintype]
ord0 [definition, in Ssreflect.fintype]
orFb [lemma, in Ssreflect.ssrbool]
orKb [lemma, in Ssreflect.ssrbool]
orNb [lemma, in Ssreflect.ssrbool]
orP [lemma, in Ssreflect.ssrbool]
orTb [lemma, in Ssreflect.ssrbool]
or3 [inductive, in Ssreflect.ssrbool]
or3P [lemma, in Ssreflect.ssrbool]
Or31 [constructor, in Ssreflect.ssrbool]
Or32 [constructor, in Ssreflect.ssrbool]
Or33 [constructor, in Ssreflect.ssrbool]
or4 [inductive, in Ssreflect.ssrbool]
or4P [lemma, in Ssreflect.ssrbool]
Or41 [constructor, in Ssreflect.ssrbool]
Or42 [constructor, in Ssreflect.ssrbool]
Or43 [constructor, in Ssreflect.ssrbool]
Or44 [constructor, in Ssreflect.ssrbool]
OtherEncodings [section, in Ssreflect.choice]
OtherEncodings.T [variable, in Ssreflect.choice]
OtherEncodings.T1 [variable, in Ssreflect.choice]
OtherEncodings.T2 [variable, in Ssreflect.choice]



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)