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

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

Visibility: public export

unVal : Singleton x -> a

Visibility: public export

.unVal : Singleton x -> a

Visibility: public export

pure : (x : a) -> Singleton x

Visibility: public export

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

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