Contribution: Karatsuba

Global Index

F

G

H

I

J

L

O

Q

R

V

W

X

Y

_

(138 entries)

Lemma Index

A

B

F

G

H

I

J

L

O

Q

R

S

U

V

W

X

Y

_

(41 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

U

V

W

X

Y

Z

_

(2 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

V

W

X

Y

Z

_

(2 entries)

Definition Index

B

E

F

G

H

I

J

L

O

Q

R

S

T

U

V

W

X

Y

_

(37 entries)

Module Index

A

B

E

F

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

(25 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(11 entries)

Library Index

A

E

F

G

H

I

J

L

M

O

Q

R

S

V

W

X

Y

_

(20 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_antisym [lemma, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_refl [lemma, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_total [lemma, in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_trans [lemma, 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_antisym [axiom, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_refl [axiom, in Karatsuba.Order.ComparisonDecOrd]
ComparisonSig.compare_trans [axiom, in Karatsuba.Order.ComparisonDecOrd]

D

DecidableOrder [library]
Discharge [library]
Distributivity [module, in Karatsuba.Order.DecidableOrder]
DistributivityA [module, in Karatsuba.Order.DecidableOrder]
DistributivityAOrd [module, in Karatsuba.Order.DecidableOrder]
DistributivityA.min_max_distr [lemma, in Karatsuba.Order.DecidableOrder]
DistributivityB [module, in Karatsuba.Order.DecidableOrder]
DistributivityBOrd [module, in Karatsuba.Order.DecidableOrder]
DistributivityB.max_min_distr [definition, in Karatsuba.Order.DecidableOrder]
DistributivityOrd [module, in Karatsuba.Order.DecidableOrder]
Dual [module, in Karatsuba.Order.DecidableOrder]
DualDistrib [module, in Karatsuba.Order.DecidableOrder]
DualOrd [module, in Karatsuba.Order.DecidableOrder]
DualOrd [module, in Karatsuba.Order.DecidableOrder]
Dual.A [definition, in Karatsuba.Order.DecidableOrder]
Dual.le [definition, in Karatsuba.Order.DecidableOrder]
Dual.le_antisym [lemma, in Karatsuba.Order.DecidableOrder]
Dual.le_refl [definition, in Karatsuba.Order.DecidableOrder]
Dual.le_total [lemma, in Karatsuba.Order.DecidableOrder]
Dual.le_trans [lemma, 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 [module, in Karatsuba.Order.DecidableOrder]
MaxOrd [module, in Karatsuba.Order.DecidableOrder]
Max.case_max [definition, in Karatsuba.Order.DecidableOrder]
Max.max [definition, in Karatsuba.Order.DecidableOrder]
Max.max_assoc [definition, in Karatsuba.Order.DecidableOrder]
Max.max_left [definition, in Karatsuba.Order.DecidableOrder]
Max.max_lub [definition, in Karatsuba.Order.DecidableOrder]
Max.max_right [definition, in Karatsuba.Order.DecidableOrder]
Max.max_sym [definition, in Karatsuba.Order.DecidableOrder]
Min [module, in Karatsuba.Order.DecidableOrder]
MinMax [module, in Karatsuba.Order.DecidableOrder]
MinMaxOrd [module, in Karatsuba.Order.DecidableOrder]
MinMaxOrd [module, in Karatsuba.Order.DecidableOrder]
MinMaxOrd [module, in Karatsuba.Order.DecidableOrder]
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_glb [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_left [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_right [lemma, in Karatsuba.Order.DecidableOrder]
Min.min_sym [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_antisym [lemma, in Karatsuba.ArithEx.Compare]
natComparision.compare_refl [lemma, in Karatsuba.ArithEx.Compare]
natComparision.compare_trans [lemma, 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.Nsplit]
PsplitAt [definition, in Karatsuba.NArithEx.Psplit]
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_antisym [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_refl [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_total [axiom, in Karatsuba.Order.DecidableOrder]
Sig.le_trans [axiom, in Karatsuba.Order.DecidableOrder]

T

TacticEx [library]
Theory [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]

Lemma Index

C

CompareDecOrd.le_antisym [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_refl [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_total [in Karatsuba.Order.ComparisonDecOrd]
CompareDecOrd.le_trans [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_antisym [in Karatsuba.Order.DecidableOrder]
Dual.le_total [in Karatsuba.Order.DecidableOrder]
Dual.le_trans [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_glb [in Karatsuba.Order.DecidableOrder]
Min.min_left [in Karatsuba.Order.DecidableOrder]
Min.min_right [in Karatsuba.Order.DecidableOrder]
Min.min_sym [in Karatsuba.Order.DecidableOrder]
multMorphism [in Karatsuba.NArithEx.Pring]

N

natComparision.compare_antisym [in Karatsuba.ArithEx.Compare]
natComparision.compare_refl [in Karatsuba.ArithEx.Compare]
natComparision.compare_trans [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]

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_left [in Karatsuba.Order.DecidableOrder]
Max.max_lub [in Karatsuba.Order.DecidableOrder]
Max.max_right [in Karatsuba.Order.DecidableOrder]
Max.max_sym [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.Nsplit]
PsplitAt [in Karatsuba.NArithEx.Psplit]
PsplitAtFast [in Karatsuba.NArithEx.Psplit]
PsplitAt2 [in Karatsuba.NArithEx.Psplit]
PsplitAt3 [in Karatsuba.NArithEx.Psplit]

Z

Zmult [in Karatsuba.Karatsuba.Zmult]

Module Index

C

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

D

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

M

Max [in Karatsuba.Order.DecidableOrder]
Max [in Karatsuba.Order.DecidableOrder]
MaxOrd [in Karatsuba.Order.DecidableOrder]
Min [in Karatsuba.Order.DecidableOrder]
MinMax [in Karatsuba.Order.DecidableOrder]
MinMaxOrd [in Karatsuba.Order.DecidableOrder]
MinMaxOrd [in Karatsuba.Order.DecidableOrder]
MinMaxOrd [in Karatsuba.Order.DecidableOrder]
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]

Axiom Index

C

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

S

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

Library Index

B

C

Coercions
Compare
Comparison
ComparisonDecOrd

D

DecidableOrder
Discharge

K

N

Nminus
Nshift
Nsize
Nsplit

P

Pring
Pshift
Psize
Psplit

T

TacticEx
Timing

U

utf8

Z

Zmult

Global Index

F

G

H

I

J

L

O

Q

R

V

W

X

Y

_

(138 entries)

Lemma Index

A

B

F

G

H

I

J

L

O

Q

R

S

U

V

W

X

Y

_

(41 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

U

V

W

X

Y

Z

_

(2 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

V

W

X

Y

Z

_

(2 entries)

Definition Index

B

E

F

G

H

I

J

L

O

Q

R

S

T

U

V

W

X

Y

_

(37 entries)

Module Index

A

B

E

F

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

(25 entries)

Axiom Index

A

B

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

(11 entries)

Library Index

A

E

F

G

H

I

J

L

M

O

Q

R

S

V

W

X

Y

_

(20 entries)