Skip to content

chore: make auto param decls of private decls private #18425

chore: make auto param decls of private decls private

chore: make auto param decls of private decls private #18425

Triggered via pull request December 10, 2025 13:13
Status Failure
Total duration 8s
Artifacts

awaiting-mathlib.yml

on: pull_request
check-awaiting-mathlib
3s
check-awaiting-mathlib
Fit to window
Zoom out
Zoom in

Annotations

1 error
check-awaiting-mathlib
PR has both "awaiting-mathlib" and "breaks-mathlib" labels.