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 (163 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 (25 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 (25 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 (20 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 (41 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 (2 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 (11 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 (2 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 (37 entries)

Global Index

A

A [definition, in Karatsuba.Karatsuba.Timing]


B

BinPosEx [library]


C

Coercions [library]
Compare [library]
CompareDecOrd [module, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.A [definition, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le [definition, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_total [lemma, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_trans [lemma, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_antisym [lemma, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_refl [lemma, in Karatsuba.Order.ComparisonDecOrd]
_ ≤ _ (order_scope) [notation, in Karatsuba.Order.ComparisonDecOrd]
compareLe [lemma, in Karatsuba.Order.Comparison]
compareLt [lemma, in Karatsuba.Order.Comparison]
Comparison [library]
ComparisonDecOrd [library]
comparisonGe [definition, in Karatsuba.Order.Comparison]
comparisonGt [definition, in Karatsuba.Order.Comparison]
comparisonLe [definition, in Karatsuba.Order.Comparison]
comparisonLt [definition, in Karatsuba.Order.Comparison]
ComparisonSig [module, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.A [axiom, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare [axiom, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_trans [axiom, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_antisym [axiom, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_refl [axiom, in Karatsuba.Order.ComparisonDecOrd]
_ ?= _ (order_scope) [notation, in Karatsuba.Order.ComparisonDecOrd]


D

DecidableOrder [library]
Discharge [library]
Distributivity [module, in Karatsuba.Order.DecidableOrder]
DistributivityA [module, in Karatsuba.Order.DecidableOrder]
DistributivityA.MinMaxOrd [module, in Karatsuba.Order.DecidableOrder]
DistributivityA.min_max_distr [lemma, in Karatsuba.Order.DecidableOrder]
DistributivityB [module, in Karatsuba.Order.DecidableOrder]
DistributivityB.DualDistrib [module, in Karatsuba.Order.DecidableOrder]
DistributivityB.DualOrd [module, in Karatsuba.Order.DecidableOrder]
DistributivityB.max_min_distr [definition, in Karatsuba.Order.DecidableOrder]
DistributivityB.MinMaxOrd [module, in Karatsuba.Order.DecidableOrder]
Distributivity.DistributivityAOrd [module, in Karatsuba.Order.DecidableOrder]
Distributivity.DistributivityBOrd [module, in Karatsuba.Order.DecidableOrder]
Distributivity.MinMaxOrd [module, in Karatsuba.Order.DecidableOrder]
Dual [module, in Karatsuba.Order.DecidableOrder]
Dual.A [definition, in Karatsuba.Order.DecidableOrder]
Dual.le [definition, in Karatsuba.Order.DecidableOrder]
Dual.le_total [lemma, in Karatsuba.Order.DecidableOrder]
Dual.le_trans [lemma, in Karatsuba.Order.DecidableOrder]
Dual.le_antisym [lemma, in Karatsuba.Order.DecidableOrder]
Dual.le_refl [definition, in Karatsuba.Order.DecidableOrder]
_ ≤ _ (order_scope) [notation, in Karatsuba.Order.DecidableOrder]


E

eqMorphism [lemma, in Karatsuba.NArithEx.Pring]


K

Karatsuba [library]
KaratsubaMult [definition, in Karatsuba.Karatsuba.Karatsuba]
KaratsubaMultCorrect [lemma, in Karatsuba.Karatsuba.Karatsuba]
KaratsubaMultCorrect1 [lemma, in Karatsuba.Karatsuba.Karatsuba]
KaratsubaMultF [definition, in Karatsuba.Karatsuba.Karatsuba]
KaratsubaStop [definition, in Karatsuba.Karatsuba.Karatsuba]


M

Max [module, in Karatsuba.Order.DecidableOrder]
Max.case_max [definition, in Karatsuba.Order.DecidableOrder]
Max.DualOrd [module, in Karatsuba.Order.DecidableOrder]
Max.max [definition, in Karatsuba.Order.DecidableOrder]
Max.Max [module, in Karatsuba.Order.DecidableOrder]
Max.max_assoc [definition, in Karatsuba.Order.DecidableOrder]
Max.max_sym [definition, in Karatsuba.Order.DecidableOrder]
Max.max_right [definition, in Karatsuba.Order.DecidableOrder]
Max.max_left [definition, in Karatsuba.Order.DecidableOrder]
Max.max_lub [definition, in Karatsuba.Order.DecidableOrder]
Min [module, in Karatsuba.Order.DecidableOrder]
MinMax [module, in Karatsuba.Order.DecidableOrder]
MinMax.MaxOrd [module, in Karatsuba.Order.DecidableOrder]
MinMax.MinOrd [module, in Karatsuba.Order.DecidableOrder]
Min.case_min [lemma, in Karatsuba.Order.DecidableOrder]
Min.min [definition, in Karatsuba.Order.DecidableOrder]
Min.min_assoc [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_sym [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_right [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_left [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_glb [lemma, in Karatsuba.Order.DecidableOrder]
multMorphism [lemma, in Karatsuba.NArithEx.Pring]


N

natComparision [module, in Karatsuba.ArithEx.Compare]
natComparision.A [definition, in Karatsuba.ArithEx.Compare]
natComparision.compare [definition, in Karatsuba.ArithEx.Compare]
natComparision.compare_trans [lemma, in Karatsuba.ArithEx.Compare]
natComparision.compare_antisym [lemma, in Karatsuba.ArithEx.Compare]
natComparision.compare_refl [lemma, in Karatsuba.ArithEx.Compare]
_ ?= _ (nat_scope) [notation, in Karatsuba.ArithEx.Compare]
natDecOrd [module, in Karatsuba.ArithEx.Compare]
Nminus [definition, in Karatsuba.NArithEx.Nminus]
Nminus [library]
Nminus_plus [lemma, in Karatsuba.NArithEx.Nminus]
Nshift [definition, in Karatsuba.NArithEx.Nshift]
Nshift [library]
NshiftExpand [lemma, in Karatsuba.NArithEx.Nshift]
Nshift2 [lemma, in Karatsuba.NArithEx.Nshift]
Nsize [definition, in Karatsuba.NArithEx.Nsize]
Nsize [library]
Nsplit [library]
NsplitAt [definition, in Karatsuba.NArithEx.Nsplit]
NsplitAtSum [lemma, in Karatsuba.NArithEx.Nsplit]


P

pairTactic [constructor, in Karatsuba.common.Discharge]
Pcompare_refl [lemma, in Karatsuba.NArithEx.BinPosEx]
plusMorphism [lemma, in Karatsuba.NArithEx.Pring]
Pminus_plus [lemma, in Karatsuba.NArithEx.BinPosEx]
Pow2 [definition, in Karatsuba.NArithEx.Pshift]
Pplus_bigger [lemma, in Karatsuba.NArithEx.BinPosEx]
Pring [library]
prodTactic [inductive, in Karatsuba.common.Discharge]
Pshift [definition, in Karatsuba.NArithEx.Pshift]
Pshift [library]
PshiftExpand [lemma, in Karatsuba.NArithEx.Pshift]
Pshift1 [lemma, in Karatsuba.NArithEx.Pshift]
Pshift2 [lemma, in Karatsuba.NArithEx.Pshift]
Pshift3 [lemma, in Karatsuba.NArithEx.Pshift]
Psize [definition, in Karatsuba.NArithEx.Psize]
Psize [library]
Psize1 [lemma, in Karatsuba.NArithEx.Psize]
Psplit [library]
PsplitAt [definition, in Karatsuba.NArithEx.Psplit]
PsplitAt [definition, in Karatsuba.NArithEx.Nsplit]
PsplitAtFast [definition, in Karatsuba.NArithEx.Psplit]
PsplitAtFastCorrect [lemma, in Karatsuba.NArithEx.Psplit]
PsplitAtSum [lemma, in Karatsuba.NArithEx.Nsplit]
PsplitAt1 [lemma, in Karatsuba.NArithEx.Psplit]
PsplitAt2 [definition, in Karatsuba.NArithEx.Psplit]
PsplitAt3 [definition, in Karatsuba.NArithEx.Psplit]


S

Sig [module, in Karatsuba.Order.DecidableOrder]
Sig.A [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_total [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_trans [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_antisym [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_refl [axiom, in Karatsuba.Order.DecidableOrder]
_ ≤ _ (order_scope) [notation, in Karatsuba.Order.DecidableOrder]


T

TacticEx [library]
Theory [module, in Karatsuba.Order.DecidableOrder]
Theory.DistributivityOrd [module, in Karatsuba.Order.DecidableOrder]
Timing [library]
trans_simp [lemma, in Karatsuba.Order.ComparisonDecOrd]
ttTactic [constructor, in Karatsuba.common.Discharge]


U

unitTactic [inductive, in Karatsuba.common.Discharge]
utf8 [library]


Z

Zmult [definition, in Karatsuba.Karatsuba.Zmult]
Zmult [library]
ZmultCorrect [lemma, in Karatsuba.Karatsuba.Zmult]


other

_ ?= _ (positive_scope) [notation, in Karatsuba.NArithEx.BinPosEx]
[ _ , _ , .. , _ ] (tactic_scope) [notation, in Karatsuba.common.Discharge]
¬ _ (type_scope) [notation, in Karatsuba.common.utf8]
_ ⇔ _ (type_scope) [notation, in Karatsuba.common.utf8]
_ ⇒ _ (type_scope) [notation, in Karatsuba.common.utf8]
_ ∧ _ (type_scope) [notation, in Karatsuba.common.utf8]
_ ∨ _ (type_scope) [notation, in Karatsuba.common.utf8]
∃ _ _ : _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∃ _ : _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∃ _ _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∃ _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ _ _ _ : _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ _ _ : _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ _ : _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ : _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ _ _ _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ _ _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
∀ _ , _ (type_scope) [notation, in Karatsuba.common.utf8]
_ ≠ _ [notation, in Karatsuba.common.utf8]



Notation Index

C

_ ≤ _ (order_scope) [in Karatsuba.Order.ComparisonDecOrd]
_ ?= _ (order_scope) [in Karatsuba.Order.ComparisonDecOrd]


D

_ ≤ _ (order_scope) [in Karatsuba.Order.DecidableOrder]


N

_ ?= _ (nat_scope) [in Karatsuba.ArithEx.Compare]


S

_ ≤ _ (order_scope) [in Karatsuba.Order.DecidableOrder]


other

_ ?= _ (positive_scope) [in Karatsuba.NArithEx.BinPosEx]
[ _ , _ , .. , _ ] (tactic_scope) [in Karatsuba.common.Discharge]
¬ _ (type_scope) [in Karatsuba.common.utf8]
_ ⇔ _ (type_scope) [in Karatsuba.common.utf8]
_ ⇒ _ (type_scope) [in Karatsuba.common.utf8]
_ ∧ _ (type_scope) [in Karatsuba.common.utf8]
_ ∨ _ (type_scope) [in Karatsuba.common.utf8]
∃ _ _ : _ , _ (type_scope) [in Karatsuba.common.utf8]
∃ _ : _ , _ (type_scope) [in Karatsuba.common.utf8]
∃ _ _ , _ (type_scope) [in Karatsuba.common.utf8]
∃ _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ _ _ _ : _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ _ _ : _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ _ : _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ : _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ _ _ _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ _ _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ _ , _ (type_scope) [in Karatsuba.common.utf8]
∀ _ , _ (type_scope) [in Karatsuba.common.utf8]
_ ≠ _ [in Karatsuba.common.utf8]



Module Index

C

CompareDecOrd [in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig [in Karatsuba.Order.ComparisonDecOrd]


D

Distributivity [in Karatsuba.Order.DecidableOrder]
DistributivityA [in Karatsuba.Order.DecidableOrder]
DistributivityA.MinMaxOrd [in Karatsuba.Order.DecidableOrder]
DistributivityB [in Karatsuba.Order.DecidableOrder]
DistributivityB.DualDistrib [in Karatsuba.Order.DecidableOrder]
DistributivityB.DualOrd [in Karatsuba.Order.DecidableOrder]
DistributivityB.MinMaxOrd [in Karatsuba.Order.DecidableOrder]
Distributivity.DistributivityAOrd [in Karatsuba.Order.DecidableOrder]
Distributivity.DistributivityBOrd [in Karatsuba.Order.DecidableOrder]
Distributivity.MinMaxOrd [in Karatsuba.Order.DecidableOrder]
Dual [in Karatsuba.Order.DecidableOrder]


M

Max [in Karatsuba.Order.DecidableOrder]
Max.DualOrd [in Karatsuba.Order.DecidableOrder]
Max.Max [in Karatsuba.Order.DecidableOrder]
Min [in Karatsuba.Order.DecidableOrder]
MinMax [in Karatsuba.Order.DecidableOrder]
MinMax.MaxOrd [in Karatsuba.Order.DecidableOrder]
MinMax.MinOrd [in Karatsuba.Order.DecidableOrder]


N

natComparision [in Karatsuba.ArithEx.Compare]
natDecOrd [in Karatsuba.ArithEx.Compare]


S

Sig [in Karatsuba.Order.DecidableOrder]


T

Theory [in Karatsuba.Order.DecidableOrder]
Theory.DistributivityOrd [in Karatsuba.Order.DecidableOrder]



Library Index

B

BinPosEx


C

Coercions
Compare
Comparison
ComparisonDecOrd


D

DecidableOrder
Discharge


K

Karatsuba


N

Nminus
Nshift
Nsize
Nsplit


P

Pring
Pshift
Psize
Psplit


T

TacticEx
Timing


U

utf8


Z

Zmult



Lemma Index

C

CompareDecOrd.le_total [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_trans [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_antisym [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_refl [in Karatsuba.Order.ComparisonDecOrd]
compareLe [in Karatsuba.Order.Comparison]
compareLt [in Karatsuba.Order.Comparison]


D

DistributivityA.min_max_distr [in Karatsuba.Order.DecidableOrder]
Dual.le_total [in Karatsuba.Order.DecidableOrder]
Dual.le_trans [in Karatsuba.Order.DecidableOrder]
Dual.le_antisym [in Karatsuba.Order.DecidableOrder]


E

eqMorphism [in Karatsuba.NArithEx.Pring]


K

KaratsubaMultCorrect [in Karatsuba.Karatsuba.Karatsuba]
KaratsubaMultCorrect1 [in Karatsuba.Karatsuba.Karatsuba]


M

Min.case_min [in Karatsuba.Order.DecidableOrder]
Min.min_assoc [in Karatsuba.Order.DecidableOrder]
Min.min_sym [in Karatsuba.Order.DecidableOrder]
Min.min_right [in Karatsuba.Order.DecidableOrder]
Min.min_left [in Karatsuba.Order.DecidableOrder]
Min.min_glb [in Karatsuba.Order.DecidableOrder]
multMorphism [in Karatsuba.NArithEx.Pring]


N

natComparision.compare_trans [in Karatsuba.ArithEx.Compare]
natComparision.compare_antisym [in Karatsuba.ArithEx.Compare]
natComparision.compare_refl [in Karatsuba.ArithEx.Compare]
Nminus_plus [in Karatsuba.NArithEx.Nminus]
NshiftExpand [in Karatsuba.NArithEx.Nshift]
Nshift2 [in Karatsuba.NArithEx.Nshift]
NsplitAtSum [in Karatsuba.NArithEx.Nsplit]


P

Pcompare_refl [in Karatsuba.NArithEx.BinPosEx]
plusMorphism [in Karatsuba.NArithEx.Pring]
Pminus_plus [in Karatsuba.NArithEx.BinPosEx]
Pplus_bigger [in Karatsuba.NArithEx.BinPosEx]
PshiftExpand [in Karatsuba.NArithEx.Pshift]
Pshift1 [in Karatsuba.NArithEx.Pshift]
Pshift2 [in Karatsuba.NArithEx.Pshift]
Pshift3 [in Karatsuba.NArithEx.Pshift]
Psize1 [in Karatsuba.NArithEx.Psize]
PsplitAtFastCorrect [in Karatsuba.NArithEx.Psplit]
PsplitAtSum [in Karatsuba.NArithEx.Nsplit]
PsplitAt1 [in Karatsuba.NArithEx.Psplit]


T

trans_simp [in Karatsuba.Order.ComparisonDecOrd]


Z

ZmultCorrect [in Karatsuba.Karatsuba.Zmult]



Constructor Index

P

pairTactic [in Karatsuba.common.Discharge]


T

ttTactic [in Karatsuba.common.Discharge]



Axiom Index

C

ComparisonSig.A [in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare [in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_trans [in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_antisym [in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_refl [in Karatsuba.Order.ComparisonDecOrd]


S

Sig.A [in Karatsuba.Order.DecidableOrder]
Sig.le [in Karatsuba.Order.DecidableOrder]
Sig.le_total [in Karatsuba.Order.DecidableOrder]
Sig.le_trans [in Karatsuba.Order.DecidableOrder]
Sig.le_antisym [in Karatsuba.Order.DecidableOrder]
Sig.le_refl [in Karatsuba.Order.DecidableOrder]



Inductive Index

P

prodTactic [in Karatsuba.common.Discharge]


U

unitTactic [in Karatsuba.common.Discharge]



Definition Index

A

A [in Karatsuba.Karatsuba.Timing]


C

CompareDecOrd.A [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le [in Karatsuba.Order.ComparisonDecOrd]
comparisonGe [in Karatsuba.Order.Comparison]
comparisonGt [in Karatsuba.Order.Comparison]
comparisonLe [in Karatsuba.Order.Comparison]
comparisonLt [in Karatsuba.Order.Comparison]


D

DistributivityB.max_min_distr [in Karatsuba.Order.DecidableOrder]
Dual.A [in Karatsuba.Order.DecidableOrder]
Dual.le [in Karatsuba.Order.DecidableOrder]
Dual.le_refl [in Karatsuba.Order.DecidableOrder]


K

KaratsubaMult [in Karatsuba.Karatsuba.Karatsuba]
KaratsubaMultF [in Karatsuba.Karatsuba.Karatsuba]
KaratsubaStop [in Karatsuba.Karatsuba.Karatsuba]


M

Max.case_max [in Karatsuba.Order.DecidableOrder]
Max.max [in Karatsuba.Order.DecidableOrder]
Max.max_assoc [in Karatsuba.Order.DecidableOrder]
Max.max_sym [in Karatsuba.Order.DecidableOrder]
Max.max_right [in Karatsuba.Order.DecidableOrder]
Max.max_left [in Karatsuba.Order.DecidableOrder]
Max.max_lub [in Karatsuba.Order.DecidableOrder]
Min.min [in Karatsuba.Order.DecidableOrder]


N

natComparision.A [in Karatsuba.ArithEx.Compare]
natComparision.compare [in Karatsuba.ArithEx.Compare]
Nminus [in Karatsuba.NArithEx.Nminus]
Nshift [in Karatsuba.NArithEx.Nshift]
Nsize [in Karatsuba.NArithEx.Nsize]
NsplitAt [in Karatsuba.NArithEx.Nsplit]


P

Pow2 [in Karatsuba.NArithEx.Pshift]
Pshift [in Karatsuba.NArithEx.Pshift]
Psize [in Karatsuba.NArithEx.Psize]
PsplitAt [in Karatsuba.NArithEx.Psplit]
PsplitAt [in Karatsuba.NArithEx.Nsplit]
PsplitAtFast [in Karatsuba.NArithEx.Psplit]
PsplitAt2 [in Karatsuba.NArithEx.Psplit]
PsplitAt3 [in Karatsuba.NArithEx.Psplit]


Z

Zmult [in Karatsuba.Karatsuba.Zmult]



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 (163 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 (25 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 (25 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 (20 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 (41 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 (2 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 (11 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 (2 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 (37 entries)