Idris2Doc : Data.MSF.Event

Data.MSF.Event

(source)
Reexports
import public Data.List.Elem
import public Data.List.Quantifiers.Extra
Definitions
data Event : Type -> Type
  A data type isomorphic to `Maybe` used to signal
  occurences of discrete events.

  Totality: total
  Visibility: public export
  Constructors:
  
NoEv : Event a
  
Ev : a -> Event a

  Hints:
  
Alternative Event
  
Applicative Event
  
Eq a => Eq (Event a)
  
Foldable Event
  
Functor Event
  
Monad Event
  
Semigroup a => Monoid (Event a)
  
Ord a => Ord (Event a)
  
Semigroup a => Semigroup (Event a)
  
Show a => Show (Event a)
  
Traversable Event
project : (0 k : {_:8949}) -> Elem k ks => Any f ks -> Event (f k)
  Try to extract a value from an n-ary sum.

  Totality: total
  Visibility: public export
maybeToEvent : Maybe a -> Event a
  Totality: total
  Visibility: public export
eventToMaybe : Event a -> Maybe a
  Totality: total
  Visibility: public export
fromEvent : Lazy a -> Event a -> a
  Totality: total
  Visibility: public export
toEvent : Bool -> Lazy a -> Event a
  Totality: total
  Visibility: public export
event : Lazy b -> Lazy (a -> b) -> Event a -> b
  Totality: total
  Visibility: public export
unionL : Event a -> Event a -> Event a
  Totality: total
  Visibility: public export
unionR : Event a -> Event a -> Event a
  Totality: total
  Visibility: public export
unionWith : (a -> a -> a) -> Event a -> Event a -> Event a
  Totality: total
  Visibility: public export
filter : (a -> Bool) -> Event a -> Event a
  Totality: total
  Visibility: public export
mapMaybe : (a -> Maybe b) -> Event a -> Event b
  Totality: total
  Visibility: public export