blob: ca72470e2be5da0bf972813f6f821130f28bee2b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
module Inky.Data.Irrelevant
public export
record Irrelevant (a : Type) where
constructor Forget
0 value : a
public export
Functor Irrelevant where
map f x = Forget (f x.value)
public export
Applicative Irrelevant where
pure x = Forget x
f <*> x = Forget (f.value x.value)
public export
Monad Irrelevant where
join x = Forget (x.value.value)
|
