0 | module Data.Singleton
 1 |
 2 | ||| The type containing only a particular value.
 3 | ||| This is useful for calculating type-level information at runtime.
 4 | public export
 5 | data Singleton : a -> Type where
 6 |      Val : (x : a) -> Singleton x
 7 |
 8 | public export %inline
 9 | reindex : (0 _ : x === y) -> Singleton x -> Singleton y
10 | reindex Refl x = x
11 |
12 | public export %inline
13 | unVal : Singleton {a} x -> a
14 | unVal $ Val x = x
15 |
16 | public export %inline
17 | (.unVal) : Singleton {a} x -> a
18 | (.unVal) = unVal
19 |
20 | -- pure and <*> implementations for idiom bracket notation
21 |
22 | public export
23 | pure : (x : a) -> Singleton x
24 | pure = Val
25 |
26 | public export
27 | (<*>) : Singleton f -> Singleton x -> Singleton (f x)
28 | Val f <*> Val x = Val (f x)
29 |