Notation.Additive

Reexports

Definitions

interface Additive1 : Type -> Type

Parameters: a
Constructor: 

MkAdditive1

Methods:

O1 : ary 0 a

(.+.) : ary 2 a

Fixity Declaration: infixl operator, level 8

Implementations:

(Additive1 a, {_:10482}) -> Additive1 a

({_:10496}, Additive1 a) -> Additive1 a

O1 : Additive1 a => ary 0 a

Totality: total
Visibility: public export

(.+.) : Additive1 a => ary 2 a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface Additive2 : Type -> Type

Parameters: a
Constructor: 

MkAdditive2

Methods:

O2 : ary 0 a

(:+:) : ary 2 a

Fixity Declaration: infixl operator, level 8

Implementations:

(Additive2 a, {_:10510}) -> Additive2 a

({_:10524}, Additive2 a) -> Additive2 a

O2 : Additive2 a => ary 0 a

Totality: total
Visibility: public export

(:+:) : Additive2 a => ary 2 a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface Additive3 : Type -> Type

Parameters: a
Constructor: 

MkAdditive3

Methods:

O3 : ary 0 a

(|+|) : ary 2 a

Fixity Declaration: infixl operator, level 8

Implementations:

(Additive3 a, {_:10538}) -> Additive3 a

({_:10552}, Additive3 a) -> Additive3 a

O3 : Additive3 a => ary 0 a

Totality: total
Visibility: public export

(|+|) : Additive3 a => ary 2 a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface AdditiveActsOn : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkAdditiveActsOn

Methods:

(+.) : ary [a, b] b

Fixity Declaration: infixl operator, level 8

(+.) : AdditiveActsOn a b => ary [a, b] b

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface AdditiveActsOn2 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkAdditiveActsOn2

Methods:

(+:) : ary [a, b] b

Fixity Declaration: infixl operator, level 8

(+:) : AdditiveActsOn2 a b => ary [a, b] b

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface AdditiveActsOn3 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkAdditiveActsOn3

Methods:

(+|) : ary [a, b] b

Fixity Declaration: infixl operator, level 8

(+|) : AdditiveActsOn3 a b => ary [a, b] b

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface AdditiveActedBy : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkAdditiveActedBy

Methods:

(.+) : ary [a, b] a

Fixity Declaration: infixl operator, level 8

(.+) : AdditiveActedBy a b => ary [a, b] a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface AdditiveActedBy2 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkAdditiveActedBy2

Methods:

(:+) : ary [a, b] a

Fixity Declaration: infixl operator, level 8

(:+) : AdditiveActedBy2 a b => ary [a, b] a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

interface AdditiveActedBy3 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkAdditiveActedBy3

Methods:

(|+) : ary [a, b] a

Fixity Declaration: infixl operator, level 8

(|+) : AdditiveActedBy3 a b => ary [a, b] a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 8

fstAdditive1 : (Additive1 a, {_:10482}) -> Additive1 a

Totality: total
Visibility: public export

sndAdditive1 : ({_:10496}, Additive1 a) -> Additive1 a

Totality: total
Visibility: public export

fstAdditive2 : (Additive2 a, {_:10510}) -> Additive2 a

Totality: total
Visibility: public export

sndAdditive2 : ({_:10524}, Additive2 a) -> Additive2 a

Totality: total
Visibility: public export

fstAdditive3 : (Additive3 a, {_:10538}) -> Additive3 a

Totality: total
Visibility: public export

sndAdditive3 : ({_:10552}, Additive3 a) -> Additive3 a

Totality: total
Visibility: public export