summaryrefslogtreecommitdiff
path: root/src/Inky/Data/Assoc.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2024-11-15 15:44:30 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2024-11-15 15:44:30 +0000
commit3caa95a139538bb07c74847ca3aba2603a03c502 (patch)
treeafa588ecffb2efd05b1202c7ce5ae6005c86b8d2 /src/Inky/Data/Assoc.idr
parent865dc549baf613e45e2f79036d54850a483fa509 (diff)
Add compilation to scheme.
Extract parser as an independent project.
Diffstat (limited to 'src/Inky/Data/Assoc.idr')
-rw-r--r--src/Inky/Data/Assoc.idr38
1 files changed, 0 insertions, 38 deletions
diff --git a/src/Inky/Data/Assoc.idr b/src/Inky/Data/Assoc.idr
deleted file mode 100644
index 0818ba3..0000000
--- a/src/Inky/Data/Assoc.idr
+++ /dev/null
@@ -1,38 +0,0 @@
-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