Skip to content

[Merged by Bors] - chore(Computability): fix whitespace#33172

Closed
harahu wants to merge 2 commits intoleanprover-community:masterfrom
harahu:chore/ws-comp
Closed

[Merged by Bors] - chore(Computability): fix whitespace#33172
harahu wants to merge 2 commits intoleanprover-community:masterfrom
harahu:chore/ws-comp

Conversation

@harahu
Copy link
Copy Markdown
Contributor

@harahu harahu commented Dec 21, 2025

Found by extending the commandStart linter to proof bodies.


Open in Gitpod

@github-actions github-actions bot added the t-computability Computability theory (TMs, DFAs, languages, grammars, etc) label Dec 21, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 21, 2025

PR summary 839af0cc3d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.


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).

@harahu harahu marked this pull request as ready for review December 22, 2025 10:32
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
bors merge

mathlib-bors bot pushed a commit that referenced this pull request Dec 22, 2025
Found by extending the commandStart linter to proof bodies.
@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 22, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 22, 2025

Build failed:

  • Post-Build Step

@bryangingechen
Copy link
Copy Markdown
Contributor

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Dec 22, 2025
Found by extending the commandStart linter to proof bodies.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 22, 2025

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Dec 22, 2025
Found by extending the commandStart linter to proof bodies.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 22, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Computability): fix whitespace [Merged by Bors] - chore(Computability): fix whitespace Dec 22, 2025
@mathlib-bors mathlib-bors bot closed this Dec 22, 2025
@harahu harahu deleted the chore/ws-comp branch December 22, 2025 18:20
kim-em pushed a commit to kim-em/mathlib4 that referenced this pull request Jan 6, 2026
Found by extending the commandStart linter to proof bodies.
goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026
Found by extending the commandStart linter to proof bodies.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-computability Computability theory (TMs, DFAs, languages, grammars, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants