git.iko.soy/Idris-dev
on master help sign in
Add index and index' to List.
bbc4037Eric Walkingshaw
libs/prelude/Prelude/List.idr+24−4
compare with master
unifiedsplit
@@ -34,10 +34,28 @@ isCons : List a -> Bool
34isCons [] = False
34isCons [] = False
35isCons (x::xs) = True
35isCons (x::xs) = True
36
36
37+--------------------------------------------------------------------------------
38+-- Length
39+--------------------------------------------------------------------------------
40+
41+length : List a -> Nat
42+length [] = 0
43+length (x::xs) = 1 + length xs
44+
37--------------------------------------------------------------------------------
45--------------------------------------------------------------------------------
38-- Indexing into lists
46-- Indexing into lists
39--------------------------------------------------------------------------------
47--------------------------------------------------------------------------------
40
48
49+index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a
50+index Z (x::xs) p = x
51+index (S n) (x::xs) p = index n xs ?indexTailProof
52+index _ [] refl impossible
53+
54+index' : (n : Nat) -> (l : List a) -> Maybe a
55+index' Z (x::xs) = Just x
56+index' (S n) (x::xs) = index' n xs
57+index' _ [] = Nothing
58+
41head : (l : List a) -> (isCons l = True) -> a
59head : (l : List a) -> (isCons l = True) -> a
42head [] refl impossible
60head [] refl impossible
43head (x::xs) p = x
61head (x::xs) p = x
@@ -112,10 +130,6 @@ list : a -> (a -> List a -> a) -> List a -> a
112list nil cons [] = nil
130list nil cons [] = nil
113list nil cons (x::xs) = cons x xs
131list nil cons (x::xs) = cons x xs
114
132
115−length : List a -> Nat
116−length [] = 0
117−length (x::xs) = 1 + length xs
118−
119--------------------------------------------------------------------------------
133--------------------------------------------------------------------------------
120-- Building (bigger) lists
134-- Building (bigger) lists
121--------------------------------------------------------------------------------
135--------------------------------------------------------------------------------
@@ -539,6 +553,12 @@ hasAnyNilFalse l = ?hasAnyNilFalseBody
539-- Proofs
553-- Proofs
540--------------------------------------------------------------------------------
554--------------------------------------------------------------------------------
541
555
556+indexTailProof = proof {
557+ intros;
558+ rewrite sym p;
559+ trivial;
560+}
561+
542lengthAppendStepCase = proof {
562lengthAppendStepCase = proof {
543 intros;
563 intros;
544 rewrite inductiveHypothesis;
564 rewrite inductiveHypothesis;