blob: 0818ba3201fee34ce2436c927512133925ec0699 (
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
27
28
29
30
31
32
33
34
35
36
37
38
|
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 a : Type) (n : String) where
constructor (:-)
0 name : String
{auto 0 prf : n = name}
value : a
public export
map : (a -> b) -> Assoc0 a n -> Assoc0 b n
map f (n :- x) = n :- f x
namespace Contexts
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
|
