Skip to content

Commit

Permalink
add difficulty description
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Mar 19, 2024
1 parent f643ddf commit e03a854
Show file tree
Hide file tree
Showing 20 changed files with 23 additions and 25 deletions.
2 changes: 1 addition & 1 deletion Src/Problem1.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/-
# Problem 1
Find the last element of a list.
(Easy) Find the last element of a list.
-/
variable {α : Type}

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem10.lean
Original file line number Diff line number Diff line change
@@ -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 --#

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem11.lean
Original file line number Diff line number Diff line change
@@ -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 --#

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem12.lean
Original file line number Diff line number Diff line change
@@ -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 --#

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem13.lean
Original file line number Diff line number Diff line change
@@ -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 --#

Expand Down
4 changes: 2 additions & 2 deletions Src/Problem14.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/-
# Problem 14
Duplicate the elements of a list.
# Problem 14
(Easy) Duplicate the elements of a list.
-/

variable {α : Type}
Expand Down
4 changes: 2 additions & 2 deletions Src/Problem15.lean
Original file line number Diff line number Diff line change
@@ -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}
Expand Down
2 changes: 1 addition & 1 deletion Src/Problem16.lean
Original file line number Diff line number Diff line change
@@ -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}

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem17.lean
Original file line number Diff line number Diff line change
@@ -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}

Expand Down
3 changes: 1 addition & 2 deletions Src/Problem2.lean
Original file line number Diff line number Diff line change
@@ -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}

Expand Down
4 changes: 2 additions & 2 deletions Src/Problem20.lean
Original file line number Diff line number Diff line change
@@ -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}

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem3.lean
Original file line number Diff line number Diff line change
@@ -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}

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem31.lean
Original file line number Diff line number Diff line change
@@ -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 :=
Expand Down
2 changes: 1 addition & 1 deletion Src/Problem32.lean
Original file line number Diff line number Diff line change
@@ -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 -/
Expand Down
2 changes: 1 addition & 1 deletion Src/Problem4.lean
Original file line number Diff line number Diff line change
@@ -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}

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem5.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/-
# Problem 5
Reverse a list.
(Easy) Reverse a list.
-/
variable {α : Type}

Expand Down
3 changes: 1 addition & 2 deletions Src/Problem6.lean
Original file line number Diff line number Diff line change
@@ -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).
-/
Expand Down
2 changes: 1 addition & 1 deletion Src/Problem7.lean
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
2 changes: 1 addition & 1 deletion Src/Problem8.lean
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
/-
# Problem 8
Eliminate consecutive duplicates of list elements.
(Intermediate) Eliminate consecutive duplicates of list elements.
-/
variable {α : Type} [BEq α]

Expand Down
2 changes: 1 addition & 1 deletion Src/Problem9.lean
Original file line number Diff line number Diff line change
@@ -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 --#

Expand Down

0 comments on commit e03a854

Please sign in to comment.