12 lines
225 B
Idris
12 lines
225 B
Idris
|
module Quox.SingletonExtra
|
||
|
|
|
||
|
|
import public Data.Singleton
|
||
|
|
|
||
|
|
public export
|
||
|
|
map : (f : a -> b) -> Singleton x -> Singleton (f x)
|
||
|
|
map f x = [|f x|]
|
||
|
|
|
||
|
|
public export
|
||
|
|
(<$>) : (f : a -> b) -> Singleton x -> Singleton (f x)
|
||
|
|
(<$>) = map
|