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