From 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 12 Nov 2024 18:05:25 +0000 Subject: Add more names. Names are good. --- src/Inky/Data/Context.idr | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'src/Inky/Data/Context.idr') 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 -- cgit v1.2.3