blob: 73c6551d0aff6de9d9d600d11d7e09891f52220f (
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
37
38
39
40
41
42
43
44
45
46
|
module Inky.Data.SnocList.Quantifiers
import public Data.SnocList.Quantifiers
import Data.List.Quantifiers
import Inky.Data.Irrelevant
import Inky.Decidable
public export
(<><) : All p xs -> All p sx -> All p (xs <>< sx)
sxp <>< [] = sxp
sxp <>< (px :: pxs) = (sxp :< px) <>< pxs
public export
head : All p (sx :< x) -> p x
head (prfs :< px) = px
public export
tail : All p (sx :< x) -> All p sx
tail (prfs :< px) = prfs
public export
HSnocList : SnocList Type -> Type
HSnocList = All id
public export
all : ((x : a) -> Dec' (p x)) -> (sx : SnocList a) -> LazyEither (All p sx) (Any (Not . p) sx)
all f [<] = True `Because` [<]
all f (sx :< x) =
map (\prfs => snd prfs :< fst prfs) (either Here There) $
both (f x) (all f sx)
public export
irrelevant : {0 sx : SnocList a} -> All (Irrelevant . p) sx -> Irrelevant (All p sx)
irrelevant [<] = Forget [<]
irrelevant (prfs :< px) = [| irrelevant prfs :< px |]
public export
relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx
relevant [<] _ = [<]
relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
public export
data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
Lin : Pairwise r [<]
(:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x)
|
