git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1427 from david-christiansen/issue/1318
8e94d31David Christiansen
CHANGELOG+1
compare with master
unifiedsplit
@@ -3,6 +3,7 @@ New in 0.9.15:
3* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.
3* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.
4* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.
4* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.
5* Stop showing irrelevant and inaccessible internal names in the interactive prover
5* Stop showing irrelevant and inaccessible internal names in the interactive prover
6+* The proof arguments in the List library functions are now implicit and solved automatically
6
7
7New in 0.9.14:
8New in 0.9.14:
8--------------
9--------------
libs/prelude/Prelude/List.idr+14−14
@@ -72,9 +72,9 @@ index' _ [] = Nothing
72
72
73||| Get the first element of a non-empty list
73||| Get the first element of a non-empty list
74||| @ ok proof that the list is non-empty
74||| @ ok proof that the list is non-empty
75−head : (l : List a) -> (ok : isCons l = True) -> a
75+head : (l : List a) -> {auto ok : isCons l = True} -> a
76−head [] refl impossible
76+head [] {ok=refl} impossible
77−head (x::xs) p = x
77+head (x::xs) {ok=p} = x
78
78
79||| Attempt to get the first element of a list. If the list is empty, return
79||| Attempt to get the first element of a list. If the list is empty, return
80||| `Nothing`.
80||| `Nothing`.
@@ -84,9 +84,9 @@ head' (x::xs) = Just x
84
84
85||| Get the tail of a non-empty list.
85||| Get the tail of a non-empty list.
86||| @ ok proof that the list is non-empty
86||| @ ok proof that the list is non-empty
87−tail : (l : List a) -> (ok : isCons l = True) -> List a
87+tail : (l : List a) -> {auto ok : isCons l = True} -> List a
88−tail [] refl impossible
88+tail [] {ok=refl} impossible
89−tail (x::xs) p = xs
89+tail (x::xs) {ok=p} = xs
90
90
91||| Attempt to get the tail of a list.
91||| Attempt to get the tail of a list.
92|||
92|||
@@ -97,10 +97,10 @@ tail' (x::xs) = Just xs
97
97
98||| Retrieve the last element of a non-empty list.
98||| Retrieve the last element of a non-empty list.
99||| @ ok proof that the list is non-empty
99||| @ ok proof that the list is non-empty
100−last : (l : List a) -> (ok : isCons l = True) -> a
100+last : (l : List a) -> {auto ok : isCons l = True} -> a
101−last [] refl impossible
101+last [] {ok=refl} impossible
102−last [x] p = x
102+last [x] {ok=p} = x
103−last (x::y::ys) p = last (y::ys) refl
103+last (x::y::ys) {ok=p} = last (y::ys) {ok=refl}
104
104
105||| Attempt to retrieve the last element of a non-empty list.
105||| Attempt to retrieve the last element of a non-empty list.
106|||
106|||
@@ -114,10 +114,10 @@ last' (x::xs) =
114
114
115||| Return all but the last element of a non-empty list.
115||| Return all but the last element of a non-empty list.
116||| @ ok proof that the list is non-empty
116||| @ ok proof that the list is non-empty
117−init : (l : List a) -> (ok : isCons l = True) -> List a
117+init : (l : List a) -> {auto ok : isCons l = True} -> List a
118−init [] refl impossible
118+init [] {ok=refl} impossible
119−init [x] p = []
119+init [x] {ok=p} = []
120−init (x::y::ys) p = x :: init (y::ys) refl
120+init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=refl}
121
121
122||| Attempt to Return all but the last element of a list.
122||| Attempt to Return all but the last element of a list.
123|||
123|||
test/error004/FunErrTest.idr+1−1
@@ -9,7 +9,7 @@ import Language.Reflection.Utils
9total
9total
10cadr : (xs : List a)
10cadr : (xs : List a)
11 -> {auto cons1 : isCons xs = True}
11 -> {auto cons1 : isCons xs = True}
12− -> {auto cons2 : isCons (tail xs cons1) = True}
12+ -> {auto cons2 : isCons (tail xs) = True}
13 -> a
13 -> a
14cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
14cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y
15cadr (x :: []) {cons1=refl} {cons2=refl} impossible
15cadr (x :: []) {cons1=refl} {cons2=refl} impossible
test/error004/expected+1−1
@@ -3,4 +3,4 @@ When elaborating argument cons1 to function FunErrTest.cadr:
3 Could not prove that [] has at least two elements.
3 Could not prove that [] has at least two elements.
4FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
4FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:
5When elaborating argument cons2 to function FunErrTest.cadr:
5When elaborating argument cons2 to function FunErrTest.cadr:
6− Could not prove that tail [(fromInteger 1)] refl has at least two elements.
6+ Could not prove that tail [(fromInteger 1)] has at least two elements.