fix: replace dropRightWhile with dropEndWhile

book/FPLean/HelloWorld/RunningAProgram.lean

@@ -142,7 +142,7 @@ def main : IO Unit := do
 
   stdout.putStrLn "How would you like to be addressed?"
   let input ← stdin.getLine
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
 
   stdout.putStrLn s!"Hello, {name}!"
 ```
@@ -192,11 +192,11 @@ The next part of the {moduleTerm}`do` block is responsible for asking the user f
 ```module (anchor:=question)
   stdout.putStrLn "How would you like to be addressed?"
   let input ← stdin.getLine
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
 ```
 
 The first line writes the question to {moduleTerm (anchor := setup)}`stdout`, the second line requests input from {moduleTerm (anchor := setup)}`stdin`, and the third line removes the trailing newline (plus any other trailing whitespace) from the input line.
-The definition of {moduleTerm (anchor := question)}`name` uses {lit}`:=`, rather than {lit}`←`, because {moduleTerm}`String.dropRightWhile` is an ordinary function on strings, rather than an {moduleTerm (anchor := sig)}`IO` action.
+The definition of {moduleTerm (anchor := question)}`name` uses {lit}`:=`, rather than {lit}`←`, because {moduleTerm}`String.dropEndWhile` is an ordinary function on strings, rather than an {moduleTerm (anchor := sig)}`IO` action.
 
 Finally, the last line in the program is:
 ```module (anchor:=answer)

book/FPLean/HelloWorld/StepByStep.lean

@@ -28,7 +28,7 @@ Start with the program from the prior section:
   let stdout ← IO.getStdout
   stdout.putStrLn "How would you like to be addressed?"
   let input ← stdin.getLine
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
   stdout.putStrLn s!"Hello, {name}!"
 ```
 :::
@@ -44,7 +44,7 @@ The first line is {anchor line1}`let stdin ← IO.getStdin`, while the remainder
   let stdout ← IO.getStdout
   stdout.putStrLn "How would you like to be addressed?"
   let input ← stdin.getLine
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
   stdout.putStrLn s!"Hello, {name}!"
 ```
 :::
@@ -70,7 +70,7 @@ Now that {anchorTerm line1}`stdin` and {anchorTerm line2}`stdout` have been foun
 ```anchor block3
   stdout.putStrLn "How would you like to be addressed?"
   let input ← stdin.getLine
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
   stdout.putStrLn s!"Hello, {name}!"
 ```
 :::
@@ -93,19 +93,19 @@ Assume the user writes “{lit}`David`”.
 The resulting line ({lit}`"David\n"`) is associated with {anchorTerm block5}`input`, where the escape sequence {lit}`\n` denotes the newline character.
 
 ```anchor block5
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
   stdout.putStrLn s!"Hello, {name}!"
 ```
 
 :::paragraph
-The next line, {anchor line5}`let name := input.dropRightWhile Char.isWhitespace`, is a {kw}`let` statement.
+The next line, {anchor line5}`let name := input.dropEndWhile Char.isWhitespace`, is a {kw}`let` statement.
 Unlike the other {kw}`let` statements in this program, it uses {anchorTerm block5}`:=` instead of {anchorTerm line4}`←`.
 This means that the expression will be evaluated, but the resulting value need not be an {moduleTerm}`IO` action and will not be executed.
-In this case, {moduleTerm}`String.dropRightWhile` takes a string and a predicate over characters and returns a new string from which all the characters at the end of the string that satisfy the predicate have been removed.
+In this case, {moduleTerm}`String.dropEndWhile` takes a string and a predicate over characters and returns a new string from which all the characters at the end of the string that satisfy the predicate have been removed.
 For example,
 
 ```anchorTerm dropBang (module := Examples.HelloWorld)
-#eval "Hello!!!".dropRightWhile (· == '!')
+#eval "Hello!!!".dropEndWhile (· == '!')
 ```
 
 yields
@@ -117,7 +117,7 @@ yields
 and
 
 ```anchorTerm dropNonLetter (module := Examples.HelloWorld)
-#eval "Hello...   ".dropRightWhile (fun c => not (c.isAlphanum))
+#eval "Hello...   ".dropEndWhile (fun c => not (c.isAlphanum))
 ```
 
 yields

book/FPLean/TypeClasses/Coercions.lean

@@ -458,8 +458,8 @@ The solution is to write a little function that cleans up the presentation by dr
 ```anchor dropDecimals
 def dropDecimals (numString : String) : String :=
   if numString.contains '.' then
-    let noTrailingZeros := numString.dropRightWhile (· == '0')
-    noTrailingZeros.dropRightWhile (· == '.')
+    let noTrailingZeros := numString.dropEndWhile (· == '0')
+    noTrailingZeros.dropEndWhile (· == '.')
   else numString
 ```
 With this definition, {anchorTerm dropDecimalExample}`dropDecimals (5 : Float).toString` yields {anchorTerm dropDecimalExample}`5`, and {anchorTerm dropDecimalExample2}`dropDecimals (5.2 : Float).toString` yields {anchorTerm dropDecimalExample2}`5.2`.

examples/Examples/Classes.lean

@@ -1669,8 +1669,8 @@ def String.separate (sep : String) (strings : List String) : String :=
 -- ANCHOR: dropDecimals
 def dropDecimals (numString : String) : String :=
   if numString.contains '.' then
-    let noTrailingZeros := numString.dropRightWhile (· == '0')
-    noTrailingZeros.dropRightWhile (· == '.')
+    let noTrailingZeros := numString.dropEndWhile (· == '0')
+    noTrailingZeros.dropEndWhile (· == '.')
   else numString
 -- ANCHOR_END: dropDecimals
 

examples/Examples/HelloWorld.lean

@@ -19,15 +19,15 @@ stop discarding
 -/
 #check_msgs in
 -- ANCHOR: dropBang
-#eval "Hello!!!".dropRightWhile (· == '!')
+#eval "Hello!!!".dropEndWhile (· == '!')
 -- ANCHOR_END: dropBang
 
 /-- info:
 "Hello"
 -/
 #check_msgs in
 -- ANCHOR: dropNonLetter
-#eval "Hello...   ".dropRightWhile (fun c => not (c.isAlphanum))
+#eval "Hello...   ".dropEndWhile (fun c => not (c.isAlphanum))
 -- ANCHOR_END: dropNonLetter
 
 

examples/hello-name/HelloName.lean

@@ -10,7 +10,7 @@ def main : IO Unit := do
   -- ANCHOR: question
   stdout.putStrLn "How would you like to be addressed?"
   let input ← stdin.getLine
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
   -- ANCHOR_END: question
 
   -- ANCHOR: answer
@@ -38,7 +38,7 @@ def mainSplit : IO Unit := do
   -- ANCHOR_END: line4
   -- ANCHOR: block5
   -- ANCHOR: line5
-  let name := input.dropRightWhile Char.isWhitespace
+  let name := input.dropEndWhile Char.isWhitespace
   -- ANCHOR_END: line5
   -- ANCHOR: block6
   -- ANCHOR: line6
@@ -54,7 +54,7 @@ def mainSplit : IO Unit := do
 -- Keep checking that they're identical
 example : main = mainSplit := by rfl
 
-example := String.dropRightWhile
+example := String.dropEndWhile
 example {α : Type} := IO α
 example : String → IO Unit := IO.println
 example := Bool