blob: a009515903108a67919d42ecb81cd812bc8adc0a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
module Inky.Data.Assoc
export
infix 2 :-
public export
record Assoc (a : Type) where
constructor (:-)
name : String
value : a
public export
Functor Assoc where
map f x = x.name :- f x.value
namespace Irrelevant
public export
record Assoc0 (0 p : a -> Type) (x : Assoc a) where
constructor (:-)
0 name : String
{auto 0 prf : x.name = name}
value : p x.value
public export
map : (forall x. p x -> q x) -> forall x. Assoc0 p x -> Assoc0 q x
map f (n :- px) = n :- f px
|
