mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
26 lines
578 B
Idris
26 lines
578 B
Idris
module Data.Singleton
|
|
|
|
||| The type containing only a particular value.
|
|
||| This is useful for calculating type-level information at runtime.
|
|
public export
|
|
data Singleton : a -> Type where
|
|
Val : (x : a) -> Singleton x
|
|
|
|
public export %inline
|
|
unVal : Singleton {a} x -> a
|
|
unVal $ Val x = x
|
|
|
|
public export %inline
|
|
(.unVal) : Singleton {a} x -> a
|
|
(.unVal) = unVal
|
|
|
|
-- pure and <*> implementations for idiom bracket notation
|
|
|
|
public export
|
|
pure : (x : a) -> Singleton x
|
|
pure = Val
|
|
|
|
public export
|
|
(<*>) : Singleton f -> Singleton x -> Singleton (f x)
|
|
Val f <*> Val x = Val (f x)
|