Notation.Multiplicative

Reexports

Definitions

interface Multiplicative1 : Type -> Type

Parameters: a
Constructor: 

MkMultiplicative1

Methods:

I1 : ary 0 a

(.*.) : ary 2 a

Fixity Declaration: infixl operator, level 9

Implementations:

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

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

I1 : Multiplicative1 a => ary 0 a

Totality: total
Visibility: public export

(.*.) : Multiplicative1 a => ary 2 a

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

interface Multiplicative2 : Type -> Type

Parameters: a
Constructor: 

MkMultiplicative2

Methods:

I2 : ary 0 a

(:*:) : ary 2 a

Fixity Declaration: infixl operator, level 9

Implementations:

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

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

I2 : Multiplicative2 a => ary 0 a

Totality: total
Visibility: public export

(:*:) : Multiplicative2 a => ary 2 a

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

interface Multiplicative3 : Type -> Type

Parameters: a
Constructor: 

MkMultiplicative3

Methods:

I3 : ary 0 a

(|*|) : ary 2 a

Fixity Declaration: infixl operator, level 9

Implementations:

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

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

I3 : Multiplicative3 a => ary 0 a

Totality: total
Visibility: public export

(|*|) : Multiplicative3 a => ary 2 a

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

interface MultiplicativeActsOn : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkMultiplicativeActsOn

Methods:

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

Fixity Declaration: infixl operator, level 9

Implementations:

(MultiplicativeActsOn a b, {_:10566}) -> MultiplicativeActsOn a b

({_:10582}, MultiplicativeActsOn a b) -> MultiplicativeActsOn a b

(*.) : MultiplicativeActsOn a b => ary [a, b] b

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

interface MultiplicativeActsOn2 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkMultiplicativeActsOn2

Methods:

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

Fixity Declaration: infixl operator, level 9

Implementations:

(MultiplicativeActsOn2 a b, {_:10598}) -> MultiplicativeActsOn2 a b

({_:10614}, MultiplicativeActsOn2 a b) -> MultiplicativeActsOn2 a b

(*:) : MultiplicativeActsOn2 a b => ary [a, b] b

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

interface MultiplicativeActsOn3 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkMultiplicativeActsOn3

Methods:

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

Fixity Declaration: infixl operator, level 9

Implementations:

(MultiplicativeActsOn3 a b, {_:10630}) -> MultiplicativeActsOn3 a b

({_:10646}, MultiplicativeActsOn3 a b) -> MultiplicativeActsOn3 a b

(*|) : MultiplicativeActsOn3 a b => ary [a, b] b

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

interface MultiplicativeActedBy : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkMultiplicativeActedBy

Methods:

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

Fixity Declaration: infixl operator, level 9

(.*) : MultiplicativeActedBy a b => ary [a, b] a

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

interface MultiplicativeActedBy2 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkMultiplicativeActedBy2

Methods:

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

Fixity Declaration: infixl operator, level 9

(:*) : MultiplicativeActedBy2 a b => ary [a, b] a

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

interface MultiplicativeActedBy3 : Type -> Type -> Type

Parameters: a, b
Constructor: 

MkMultiplicativeActedBy3

Methods:

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

Fixity Declaration: infixl operator, level 9

(|*) : MultiplicativeActedBy3 a b => ary [a, b] a

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

fstMultiplicative1 : (Multiplicative1 a, {_:10482}) -> Multiplicative1 a

Totality: total
Visibility: public export

sndMultiplicative1 : ({_:10496}, Multiplicative1 a) -> Multiplicative1 a

Totality: total
Visibility: public export

fstMultiplicative2 : (Multiplicative2 a, {_:10510}) -> Multiplicative2 a

Totality: total
Visibility: public export

sndMultiplicative2 : ({_:10524}, Multiplicative2 a) -> Multiplicative2 a

Totality: total
Visibility: public export

fstMultiplicative3 : (Multiplicative3 a, {_:10538}) -> Multiplicative3 a

Totality: total
Visibility: public export

sndMultiplicative3 : ({_:10552}, Multiplicative3 a) -> Multiplicative3 a

Totality: total
Visibility: public export

fstMultiplicativeActsOn : (MultiplicativeActsOn a b, {_:10566}) -> MultiplicativeActsOn a b

Totality: total
Visibility: public export

sndMultiplicativeActsOn : ({_:10582}, MultiplicativeActsOn a b) -> MultiplicativeActsOn a b

Totality: total
Visibility: public export

fstMultiplicativeActsOn2 : (MultiplicativeActsOn2 a b, {_:10598}) -> MultiplicativeActsOn2 a b

Totality: total
Visibility: public export

sndMultiplicativeActsOn2 : ({_:10614}, MultiplicativeActsOn2 a b) -> MultiplicativeActsOn2 a b

Totality: total
Visibility: public export

fstMultiplicativeActsOn3 : (MultiplicativeActsOn3 a b, {_:10630}) -> MultiplicativeActsOn3 a b

Totality: total
Visibility: public export

sndMultiplicativeActsOn3 : ({_:10646}, MultiplicativeActsOn3 a b) -> MultiplicativeActsOn3 a b

Totality: total
Visibility: public export