blob: 494e8cc522acebbc436db0e0b778b9b90c2a4fad (
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
|
module Inky.Data.SnocList
import public Data.SnocList
import public Data.SnocList.Operations
import Inky.Decidable.Maybe
public export
data LengthOf : SnocList a -> Type where
Z : LengthOf [<]
S : LengthOf sx -> LengthOf (sx :< x)
%name LengthOf len
public export
lengthOfAppend : LengthOf sx -> LengthOf sy -> LengthOf (sx ++ sy)
lengthOfAppend len1 Z = len1
lengthOfAppend len1 (S len2) = S (lengthOfAppend len1 len2)
public export
lengthOf : (sx : SnocList a) -> LengthOf sx
lengthOf [<] = Z
lengthOf (sx :< x) = S (lengthOf sx)
export
lengthUnique : (len1, len2 : LengthOf sx) -> len1 = len2
lengthUnique Z Z = Refl
lengthUnique (S len1) (S len2) = cong S $ lengthUnique len1 len2
export
isSnoc : (sx : SnocList a) -> Proof (SnocList a, a) (\syy => sx = fst syy :< snd syy) (sx = [<])
isSnoc [<] = Nothing `Because` Refl
isSnoc (sx :< x) = Just (sx, x) `Because` Refl
public export
replicate : Nat -> a -> SnocList a
replicate 0 x = [<]
replicate (S n) x = replicate n x :< x
public export
lengthOfReplicate : (n : Nat) -> (0 x : a) -> LengthOf (replicate n x)
lengthOfReplicate 0 x = Z
lengthOfReplicate (S k) x = S (lengthOfReplicate k x)
|
