blob: 0d3df992b7b318329fcaea1c3e3f2a28212815b3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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
|
