Skip to content

Commit

Permalink
Create Probrem4.lean
Browse files Browse the repository at this point in the history
  • Loading branch information
csharpython authored Mar 17, 2024
1 parent b99fd35 commit 8fd676c
Showing 1 changed file with 21 additions and 0 deletions.
21 changes: 21 additions & 0 deletions Src/Probrem4.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
/-
# Problem 4
Find the number of elements in a list.
-/

variable {α : Type}

def myLength (l : List α) : Nat :=
--sorry
List.length l
--sorry

-- The following is a test case, you don't need to edit it.

example : myLength [123, 456, 789] = 3 := by rfl

example : myLength ([] : List α) = 0 := by rfl

example : myLength [1,1,1,1,1,1,1,1,1,1,1,1] = 12 := by rfl

example : myLength ['w','x', 'y', 'z'] = 4 := by rfl

0 comments on commit 8fd676c

Please sign in to comment.