Skip to content

feat: Time Complexity of List.Length#486

Open
cjrl wants to merge 5 commits intoleanprover:mainfrom
cjrl:list-length-time
Open

feat: Time Complexity of List.Length#486
cjrl wants to merge 5 commits intoleanprover:mainfrom
cjrl:list-length-time

Conversation

@cjrl
Copy link
Copy Markdown

@cjrl cjrl commented Apr 12, 2026

Following the contribution guide it seems that a useful place to contribute is with TimeM implementations for data structure algorithms.

As a starting point I proved the very basic result List.length's time complexity is linear in the length of List. As far as I could tell this result was not in CSLib yet.

I followed the structure of the merge sort file.

@ctchou
Copy link
Copy Markdown
Collaborator

ctchou commented Apr 12, 2026

I think the files of this PR should be put under Cslib/Algorithms/Lean, perhaps in a ListLength subdirectory.

@cjrl
Copy link
Copy Markdown
Author

cjrl commented Apr 12, 2026

@ctchou Thanks, have moved to the Cslib/Algorithms/Lean/ListLength folder.

@ctchou ctchou changed the title feat(Foundations/Data/List) Time Complexity of List.Length feat: Time Complexity of List.Length Apr 12, 2026
@ctchou
Copy link
Copy Markdown
Collaborator

ctchou commented Apr 12, 2026

I change the title of this PR to remove the out-dated pathname.

Comment thread Cslib/Algorithms/Lean/ListLength/Basic.lean Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants