Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 26 insertions, 0 deletions

diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
new file mode 100644
index 0000000..a009515
--- /dev/null
+++ b/src/Inky/Data/Assoc.idr
@@ -0,0 +1,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