Skip to content

refactor(Data/Last): move Mathlib.Tactic.BicategoryLike.pairs to List.consecutivePairs#35829

Open
IvanRenison wants to merge 3 commits intoleanprover-community:masterfrom
IvanRenison:List.pairs
Open

refactor(Data/Last): move Mathlib.Tactic.BicategoryLike.pairs to List.consecutivePairs#35829
IvanRenison wants to merge 3 commits intoleanprover-community:masterfrom
IvanRenison:List.pairs

Conversation

@IvanRenison
Copy link
Collaborator

@IvanRenison IvanRenison commented Feb 26, 2026

Moves:

  • Mathlib.Tactic.BicategoryLike.pairs -> List.consecutivePairs

Open in Gitpod

@github-actions
Copy link

github-actions bot commented Feb 26, 2026

PR summary 9b809f3970

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ consecutivePairs

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 scripts/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@IvanRenison IvanRenison added the t-data Data (lists, quotients, numbers, etc) label Feb 26, 2026
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 27, 2026
@IvanRenison IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 27, 2026
@SnirBroshi
Copy link
Collaborator

About the name: Python calls it pairwise, Rust calls it windows(2).

@IvanRenison IvanRenison changed the title refactor(Data/Last): move Mathlib.Tactic.BicategoryLike.pairs to List.pairs refactor(Data/Last): move Mathlib.Tactic.BicategoryLike.pairs to List.consecutivePairs Feb 28, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants