Skip to content

chore: remove unused simp arguments in SuccSuccAbove - #1703

Merged
zhikaip merged 1 commit into
leanprover-community:masterfrom
nateabr:fix-succsuccabove-simp-args
Sep 30, 2026
Merged

zhikaip merged 1 commit into
leanprover-community:masterfrom
nateabr:fix-succsuccabove-simp-args

chore: remove unused simp arguments in SuccSuccAbove

b4588e8
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning and 1 notice
Python based style linter
succeeded Sep 30, 2026 in 17s