Data.Singleton

Definitions

data Singleton : a -> Type

  The type containing only a particular value.
  This is useful for calculating type-level information at runtime.

Totality: total
Visibility: public export
Constructor: 

Val : (x : a) -> Singleton x

Hints:

DecEq (Singleton v)

Eq (Singleton v)

Monoid (Singleton v)

Ord (Singleton v)

Semigroup (Singleton v)

Show a => Show (Singleton v)

reindex : (0 _ : x = y) -> Singleton x -> Singleton y

Totality: total
Visibility: public export

unVal : Singleton x -> a

Totality: total
Visibility: public export

.unVal : Singleton x -> a

Totality: total
Visibility: public export

pure : (x : a) -> Singleton x

Totality: total
Visibility: public export

(<*>) : Singleton f -> Singleton x -> Singleton (f x)

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