Skip to content

feat(Data/List/RunLength): run-length encoding#17105

Closed
vihdzp wants to merge 25 commits intomasterfrom
vi.RLE
Closed

feat(Data/List/RunLength): run-length encoding#17105
vihdzp wants to merge 25 commits intomasterfrom
vi.RLE

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Sep 24, 2024 •
edited
Loading

We define the run-length encoding of a list. We provide a basic API, as well as a recursion principle.

Open in Gitpod

@vihdzp vihdzp added WIP Work in progress t-data Data (lists, quotients, numbers, etc) labels Sep 24, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 24, 2024 •
edited
Loading

PR summary a324b4ff16

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Data.List.SplitBy 1
Mathlib.Data.List.RunLength 290

Declarations diff

+ RunLength
+ chain'_runLength
+ flatten_map_runLength
+ head_flatten_of_head_ne_nil
+ runLengthRecOn
+ runLengthRecOn_append
+ runLengthRecOn_nil
+ runLength_append
+ runLength_append_cons
+ runLength_eq_nil
+ runLength_flatten_map
+ runLength_inj
+ runLength_injective
+ runLength_nil
+ runLength_replicate
+ splitBy_append
+ splitBy_append_cons
+ splitBy_beq
+ splitBy_eq_iff
+ splitBy_eq_nil_iff
+ splitBy_flatten
+ splitBy_of_chain'
+ splitBy_singleton

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 24, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Sep 24, 2024 •
edited
Loading

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 7, 2024
@vihdzp vihdzp removed the WIP Work in progress label Nov 12, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 12, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 4, 2025
@YaelDillies YaelDillies deleted the vi.RLE branch October 25, 2025 10:40
@vihdzp vihdzp mentioned this pull request Oct 25, 2025
Open
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@vihdzp @mathlib4-dependent-issues-bot @YaelDillies @leanprover-community-bot-assistant