@@ -33,10 +33,28 @@ isCons : List a -> Bool
3333isCons [] = False
3434isCons (x::xs) = True
3535
36+--------------------------------------------------------------------------------
37+-- Length
38+--------------------------------------------------------------------------------
39+
40+length : List a -> Nat
41+length [] = 0
42+length (x::xs) = 1 + length xs
43+
3644--------------------------------------------------------------------------------
3745-- Indexing into lists
3846--------------------------------------------------------------------------------
3947
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+
4058head : (l : List a) -> (isCons l = True) -> a
4159head [] refl impossible
4260head (x::xs) p = x
@@ -111,10 +129,6 @@ list : a -> (a -> List a -> a) -> List a -> a
111129list nil cons [] = nil
112130list nil cons (x::xs) = cons x xs
113131
114−length : List a -> Nat
115−length [] = 0
116−length (x::xs) = 1 + length xs
117−
118132--------------------------------------------------------------------------------
119133-- Building (bigger) lists
120134--------------------------------------------------------------------------------
@@ -538,6 +552,12 @@ hasAnyNilFalse l = ?hasAnyNilFalseBody
538552-- Proofs
539553--------------------------------------------------------------------------------
540554
555+indexTailProof = proof {
556+ intros;
557+ rewrite sym p;
558+ trivial;
559+}
560+
541561lengthAppendStepCase = proof {
542562 intros;
543563 rewrite inductiveHypothesis;