@@ -72,9 +72,9 @@ index' _ [] = Nothing
7272
7373||| Get the first element of a non-empty list
7474||| @ ok proof that the list is non-empty
75−head : (l : List a) -> (ok : isCons l = True) -> a
76−head [] refl impossible
77−head (x::xs) p = x
75+head : (l : List a) -> {auto ok : isCons l = True} -> a
76+head [] {ok=refl} impossible
77+head (x::xs) {ok=p} = x
7878
7979||| Attempt to get the first element of a list. If the list is empty, return
8080||| `Nothing`.
@@ -84,9 +84,9 @@ head' (x::xs) = Just x
8484
8585||| Get the tail of a non-empty list.
8686||| @ ok proof that the list is non-empty
87−tail : (l : List a) -> (ok : isCons l = True) -> List a
88−tail [] refl impossible
89−tail (x::xs) p = xs
87+tail : (l : List a) -> {auto ok : isCons l = True} -> List a
88+tail [] {ok=refl} impossible
89+tail (x::xs) {ok=p} = xs
9090
9191||| Attempt to get the tail of a list.
9292|||
@@ -97,10 +97,10 @@ tail' (x::xs) = Just xs
9797
9898||| Retrieve the last element of a non-empty list.
9999||| @ ok proof that the list is non-empty
100−last : (l : List a) -> (ok : isCons l = True) -> a
101−last [] refl impossible
102−last [x] p = x
103−last (x::y::ys) p = last (y::ys) refl
100+last : (l : List a) -> {auto ok : isCons l = True} -> a
101+last [] {ok=refl} impossible
102+last [x] {ok=p} = x
103+last (x::y::ys) {ok=p} = last (y::ys) {ok=refl}
104104
105105||| Attempt to retrieve the last element of a non-empty list.
106106|||
@@ -114,10 +114,10 @@ last' (x::xs) =
114114
115115||| Return all but the last element of a non-empty list.
116116||| @ ok proof that the list is non-empty
117−init : (l : List a) -> (ok : isCons l = True) -> List a
118−init [] refl impossible
119−init [x] p = []
120−init (x::y::ys) p = x :: init (y::ys) refl
117+init : (l : List a) -> {auto ok : isCons l = True} -> List a
118+init [] {ok=refl} impossible
119+init [x] {ok=p} = []
120+init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=refl}
121121
122122||| Attempt to Return all but the last element of a list.
123123|||