Idris2Doc : Control.ApplicativeB

Control.ApplicativeB

(source)

Definitions

interface ApplicativeB : (k : Type) -> ((k -> Type) -> Type) -> Type
Parameters: k, t
Constraints: FunctorB k t
Constructor: 
MkApplicativeB

Methods:
bpure_ : ((0 a : k) -> f a) -> t f
bprod : t f -> t g -> t (\x => (f x, g x))
bpure_ : ApplicativeB k t => ((0 a : k) -> f a) -> t f
Totality: total
Visibility: public export
bprod : ApplicativeB k t => t f -> t g -> t (\x => (f x, g x))
Totality: total
Visibility: public export
bpure : ApplicativeB k t => f a -> t f
Totality: total
Visibility: public export
bempty : Alternative f => ApplicativeB k t => t (f . g)
Totality: total
Visibility: public export
bzipWith : ApplicativeB k t => (f a -> g a -> h a) -> t f -> t g -> t h
Totality: total
Visibility: public export
bzipWith3 : ApplicativeB k t => (f a -> g a -> h a -> i a) -> t f -> t g -> t h -> t i
Totality: total
Visibility: public export
pure : ApplicativeB k t => f a -> t f
Totality: total
Visibility: public export
(<*>) : ApplicativeB k t => t (\x => f x -> g x) -> t f -> t g
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 3