diff --git a/Src/Problem1.lean b/Src/Problem1.lean index 29a2809..1faf0ec 100644 --- a/Src/Problem1.lean +++ b/Src/Problem1.lean @@ -1,6 +1,6 @@ /- # Problem 1 -Find the last element of a list. +(Easy) Find the last element of a list. -/ variable {α : Type} diff --git a/Src/Problem10.lean b/Src/Problem10.lean index e2e6a93..7ccd0f5 100644 --- a/Src/Problem10.lean +++ b/Src/Problem10.lean @@ -1,6 +1,6 @@ /- # Problem 10 -Use the result of Problem 9 to implement the so-called run-length encoding data compression method. Consecutive duplicates of elements are encoded as lists `(N, E)` where `N` is the number of duplicates of the element `E`. +(Easy) Use the result of Problem 9 to implement the so-called run-length encoding data compression method. Consecutive duplicates of elements are encoded as lists `(N, E)` where `N` is the number of duplicates of the element `E`. -/ namespace P10 --# diff --git a/Src/Problem11.lean b/Src/Problem11.lean index 9f47750..ee329a5 100644 --- a/Src/Problem11.lean +++ b/Src/Problem11.lean @@ -1,6 +1,6 @@ /- # Problem 11 -Modify the result of problem 10 in such a way that if an element has no duplicates it is simply copied into the result list. Only elements with duplicates are transferred as `(N E)` lists. +(Easy) Modify the result of problem 10 in such a way that if an element has no duplicates it is simply copied into the result list. Only elements with duplicates are transferred as `(N E)` lists. -/ namespace P11 --# diff --git a/Src/Problem12.lean b/Src/Problem12.lean index 0966a08..1fe963a 100644 --- a/Src/Problem12.lean +++ b/Src/Problem12.lean @@ -1,6 +1,6 @@ /- # Problem 12 -Given a run-length code list generated as specified in problem 11. Construct its uncompressed version. +(Intermediate) Given a run-length code list generated as specified in problem 11. Construct its uncompressed version. -/ namespace P12 --# diff --git a/Src/Problem13.lean b/Src/Problem13.lean index 0a144df..98d311c 100644 --- a/Src/Problem13.lean +++ b/Src/Problem13.lean @@ -1,6 +1,6 @@ /- # Problem 13 -Implement the so-called run-length encoding data compression method directly. I.e. don't explicitly create the sublists containing the duplicates, as in problem 9, but only count them. As in problem P11, simplify the result list by replacing the singleton lists `(1 X)` by `X`. +(Intermediate) Implement the so-called run-length encoding data compression method directly. I.e. don't explicitly create the sublists containing the duplicates, as in problem 9, but only count them. As in problem P11, simplify the result list by replacing the singleton lists `(1 X)` by `X`. -/ namespace P13 --# diff --git a/Src/Problem14.lean b/Src/Problem14.lean index ba0f195..87bc255 100644 --- a/Src/Problem14.lean +++ b/Src/Problem14.lean @@ -1,6 +1,6 @@ /- - # Problem 14 - Duplicate the elements of a list. +# Problem 14 +(Easy) Duplicate the elements of a list. -/ variable {α : Type} diff --git a/Src/Problem15.lean b/Src/Problem15.lean index f13b1a9..3bc1423 100644 --- a/Src/Problem15.lean +++ b/Src/Problem15.lean @@ -1,6 +1,6 @@ /- - # Problem 15 - Replicate the elements of a list a given number of times. +# Problem 15 +(Intermediate) Replicate the elements of a list a given number of times. -/ variable {α : Type} diff --git a/Src/Problem16.lean b/Src/Problem16.lean index d429191..f253b2b 100644 --- a/Src/Problem16.lean +++ b/Src/Problem16.lean @@ -1,6 +1,6 @@ /- # Problem 16 -Drop every N'th element from a list. +(Intermediate) Drop every N'th element from a list. -/ variable {α : Type} diff --git a/Src/Problem17.lean b/Src/Problem17.lean index cf49524..6b93a32 100644 --- a/Src/Problem17.lean +++ b/Src/Problem17.lean @@ -1,6 +1,6 @@ /- # Problem 17 -Split a list into two parts; the length of the first part is given. +(Easy) Split a list into two parts; the length of the first part is given. -/ variable {α : Type} diff --git a/Src/Problem2.lean b/Src/Problem2.lean index c93d419..1fa870b 100644 --- a/Src/Problem2.lean +++ b/Src/Problem2.lean @@ -1,7 +1,6 @@ /- # Problem 2 - -Find the last-but-one (or second-last) element of a list. +(Easy) Find the last-but-one (or second-last) element of a list. -/ variable {α : Type} diff --git a/Src/Problem20.lean b/Src/Problem20.lean index a29207e..71763db 100644 --- a/Src/Problem20.lean +++ b/Src/Problem20.lean @@ -1,6 +1,6 @@ /- - # Problem 20 - Remove the K'th element from a list. +# Problem 20 +(Easy) Remove the K'th element from a list. -/ variable {α : Type} diff --git a/Src/Problem3.lean b/Src/Problem3.lean index a6d4ae4..b7c166d 100644 --- a/Src/Problem3.lean +++ b/Src/Problem3.lean @@ -1,6 +1,6 @@ /- # Problem 3 -Find the K'th element of a list. +(Easy) Find the K'th element of a list. -/ variable {α : Type} diff --git a/Src/Problem31.lean b/Src/Problem31.lean index c6c49bf..ed59341 100644 --- a/Src/Problem31.lean +++ b/Src/Problem31.lean @@ -1,6 +1,6 @@ /- # Problem 31 -Determine whether a given integer number is prime. +(Intermediate) Determine whether a given integer number is prime. -/ def isPrime (n : Nat) : Bool := diff --git a/Src/Problem32.lean b/Src/Problem32.lean index 29fcef5..58e11dc 100644 --- a/Src/Problem32.lean +++ b/Src/Problem32.lean @@ -1,6 +1,6 @@ /- # Problem 32 -Determine the greatest common divisor of two positive integer numbers. Use the Euclid's algorithm. +(Intermediate) Determine the greatest common divisor of two positive integer numbers. Use the Euclid's algorithm. -/ /-- Euclidean algorithm -/ diff --git a/Src/Problem4.lean b/Src/Problem4.lean index 864b912..2e8c3d9 100644 --- a/Src/Problem4.lean +++ b/Src/Problem4.lean @@ -1,6 +1,6 @@ /- # Problem 4 -Find the number of elements in a list. +(Easy) Find the number of elements in a list. -/ variable {α : Type} diff --git a/Src/Problem5.lean b/Src/Problem5.lean index d65cef9..161bb2f 100644 --- a/Src/Problem5.lean +++ b/Src/Problem5.lean @@ -1,6 +1,6 @@ /- # Problem 5 -Reverse a list. +(Easy) Reverse a list. -/ variable {α : Type} diff --git a/Src/Problem6.lean b/Src/Problem6.lean index b323350..a752f8d 100644 --- a/Src/Problem6.lean +++ b/Src/Problem6.lean @@ -1,7 +1,6 @@ /- # Problem 6 - -Find out whether a list is a palindrome. +(Easy) Find out whether a list is a palindrome. Hint: A palindrome can be read forward or backward; e.g. (x a m a x). -/ diff --git a/Src/Problem7.lean b/Src/Problem7.lean index 928b222..5fe3cb9 100644 --- a/Src/Problem7.lean +++ b/Src/Problem7.lean @@ -1,6 +1,6 @@ /- # Problem 7 -Flatten a nested list structure. +(Intermediate) Flatten a nested list structure. -/ -- We have to define a new data type, because lists in Lean are homogeneous. diff --git a/Src/Problem8.lean b/Src/Problem8.lean index 7520a65..6428293 100644 --- a/Src/Problem8.lean +++ b/Src/Problem8.lean @@ -1,6 +1,6 @@ /- # Problem 8 -Eliminate consecutive duplicates of list elements. +(Intermediate) Eliminate consecutive duplicates of list elements. -/ variable {α : Type} [BEq α] diff --git a/Src/Problem9.lean b/Src/Problem9.lean index dd0ca2c..abdb335 100644 --- a/Src/Problem9.lean +++ b/Src/Problem9.lean @@ -1,6 +1,6 @@ /- # Problem 9 -Pack consecutive duplicates of list elements into sublists. +(Intermediate) Pack consecutive duplicates of list elements into sublists. -/ namespace P9 --#