Skip to content
lint and suggest

chore(Data/Finset): split Basic.lean into many smaller files #65085

Sign in to view logs

chore(Data/Finset): split Basic.lean into many smaller files

chore(Data/Finset): split Basic.lean into many smaller files #65085

Triggered via pull request November 5, 2024 11:08
@VierkantorVierkantor
synchronize #18610
split-Finset.Basic
Status Success
Total duration 1m 26s
Artifacts –

lint_and_suggest_pr.yml

on: pull_request
Lint style
1m 18s
Lint style
Check all files imported
34s
Check all files imported
Fit to window
Zoom out
Zoom in