diff options
author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-15 15:44:30 +0000 |
---|---|---|
committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-11-15 15:44:30 +0000 |
commit | 3caa95a139538bb07c74847ca3aba2603a03c502 (patch) | |
tree | afa588ecffb2efd05b1202c7ce5ae6005c86b8d2 /src/Inky/Data/Assoc.idr | |
parent | 865dc549baf613e45e2f79036d54850a483fa509 (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.idr | 38 |
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 |