Make everything relevant.

Too few proofs were relevant. Now they are.

1 files changed, 36 insertions, 0 deletions

diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr
new file mode 100644
index 0000000..0d3df99
--- /dev/null
+++ b/src/Inky/Data/Context.idr
@@ -0,0 +1,36 @@
+module Inky.Data.Context
+
+import public Inky.Data.Assoc
+import public Inky.Data.SnocList
+
+import Inky.Data.SnocList.Quantifiers
+
+-- Contexts --------------------------------------------------------------------
+
+public export
+Context : Type -> Type
+Context a = SnocList (Assoc a)
+
+public export
+(.names) : Context a -> SnocList String
+[<].names = [<]
+(ctx :< nx).names = ctx.names :< nx.name
+
+export
+mapNames : (0 f : a -> b) -> (ctx : Context a) -> (map (map f) ctx).names = ctx.names
+mapNames f [<] = Refl
+mapNames f (ctx :< nx) = cong (:< nx.name) $ mapNames f ctx
+
+-- Construction ----------------------------------------------------------------
+
+public export
+fromAll : (ctx : Context a) -> All (const b) ctx.names -> Context b
+fromAll [<] [<] = [<]
+fromAll (ctx :< (n :- _)) (sx :< x) = fromAll ctx sx :< (n :- x)
+
+export
+fromAllNames :
+  (ctx : Context a) -> (sx : All (const b) ctx.names) ->
+  (fromAll ctx sx).names = ctx.names
+fromAllNames [<] [<] = Refl
+fromAllNames (ctx :< (n :- _)) (sx :< x) = cong (:< n) $ fromAllNames ctx sx