Skip to content

fix: replace dropRightWhile with dropEndWhile#264

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

fix: replace dropRightWhile with dropEndWhile#264
Neptunium931 wants to merge 1 commit intoleanprover:masterfrom
Neptunium931:dropRightWhile/deprecated

Conversation

@Neptunium931
Copy link

@Neptunium931 Neptunium931 commented Feb 6, 2026

Hello, thank you for all the work that has allowed me to discover Lean, but it seems that there is a use of a deprecated function dropRightWhile

def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout

  stdout.putStrLn "How would you like to be addressed?"
  let input ← stdin.getLine
  let name := input.dropRightWhile Char.isWhitespace

  stdout.putStrLn s!"Hello, {name}!"
lean --run hello.lean
hello.lean:7:20: warning: `String.dropRightWhile` has been deprecated: Use `String.dropEndWhile` instead

Note: The updated constant has a different type:
  {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
instead of
  String → (Char → Bool) → String

I used the following command to make the modification; I think I've replaced it in the only necessary place.

find . -type f -iname *.lean -exec sed -i 's/dropRightWhile/dropEndWhile/g' {} +

lean version :

$ lean --version
Lean (version 4.29.0-pre, commit 6cf632bef2d64028df39e3cb790deb9e6e431067, Release)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant