Data.Some

A module defining the `Some` type

Reexports

Definitions

data Some : (t -> Type) -> Type

  Wraps a dependent type, so that its parameter is hidden.
  Values of dependent types, wrapped this way, have the same type
  @ f the type constructor of types of the wrapped values.

Totality: total
Visibility: public export
Constructor: 

MkSome : f a -> Some f

  Hide the type parameter of the type of a value
  @ a the parameter of the type of the wrapped value
  @ x the wrapped value

Hints:

DEq f => Eq (Some f)

Applicative m => Monoid (Some m)

DOrd f => Ord (Some f)

Applicative m => Semigroup (Some m)

DShow f => Show (Some f)

withSome : Some f -> (f x -> b) -> b

  Apply a dependency-removing function to the value wrapped in `Some` and
  drop the wrapper

Visibility: export

withSomeM : Monad m => m (Some f) -> (f x -> m b) -> m b

  Monadic 'withSome'.

Visibility: export

foldSome : (tag a -> b) -> Some tag -> b

  | `'flip' 'withSome'`

Visibility: export

map : (f a -> g a) -> Some f -> Some g

  Apply a function to the wrapped value

Visibility: export

traverseSome : Functor m => (f a -> m (g a)) -> Some f -> m (Some g)

  Traverse over argument.

Visibility: export