Skip to content

fix: replace dropRightWhile with dropEndWhile - #264

Open
Neptunium931 wants to merge 1 commit into
leanprover:masterfrom
Neptunium931:dropRightWhile/deprecated
Open

Neptunium931 wants to merge 1 commit into
leanprover:masterfrom
Neptunium931:dropRightWhile/deprecated

Commits

Commits on Feb 6, 2026