@@ -34,10 +34,28 @@ isCons : List a -> Bool
3434isCons [] = False
3535isCons (x::xs) = True
3636
37+--------------------------------------------------------------------------------
38+-- Length
39+--------------------------------------------------------------------------------
40+
41+length : List a -> Nat
42+length [] = 0
43+length (x::xs) = 1 + length xs
44+
3745--------------------------------------------------------------------------------
3846-- Indexing into lists
3947--------------------------------------------------------------------------------
4048
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+
4159head : (l : List a) -> (isCons l = True) -> a
4260head [] refl impossible
4361head (x::xs) p = x
@@ -112,10 +130,6 @@ list : a -> (a -> List a -> a) -> List a -> a
112130list nil cons [] = nil
113131list nil cons (x::xs) = cons x xs
114132
115−length : List a -> Nat
116−length [] = 0
117−length (x::xs) = 1 + length xs
118−
119133--------------------------------------------------------------------------------
120134-- Building (bigger) lists
121135--------------------------------------------------------------------------------
@@ -539,6 +553,12 @@ hasAnyNilFalse l = ?hasAnyNilFalseBody
539553-- Proofs
540554--------------------------------------------------------------------------------
541555
556+indexTailProof = proof {
557+ intros;
558+ rewrite sym p;
559+ trivial;
560+}
561+
542562lengthAppendStepCase = proof {
543563 intros;
544564 rewrite inductiveHypothesis;