Add more names. Names are good.

1 files changed, 6 insertions, 8 deletions

diff --git a/src/Inky/Data/Context.idr b/src/Inky/Data/Context.idr
index 0d3df99..4c5f6cf 100644
--- a/src/Inky/Data/Context.idr
+++ b/src/Inky/Data/Context.idr
@@ -24,13 +24,11 @@ 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)
+fromAll : {sx : SnocList String} -> All (Assoc0 a) sx -> Context a
+fromAll [<] = [<]
+fromAll {sx = sx :< n} (ctx :< (_ :- x)) = fromAll ctx :< (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
+fromAllNames : {sx : SnocList String} -> (ctx : All (Assoc0 a) sx) -> (fromAll ctx).names = sx
+fromAllNames [<] = Refl
+fromAllNames {sx = sx :< n} (ctx :< (k :- x)) = cong (:< n) $ fromAllNames ctx