From e00aff6bd22168468eb534c2eb5f5d9d7a79c0c9 Mon Sep 17 00:00:00 2001 From: neptumiun Date: Fri, 6 Feb 2026 11:51:36 +0100 Subject: [PATCH] fix: replace dropRightWhile with dropEndWhile --- book/FPLean/HelloWorld/RunningAProgram.lean | 6 +++--- book/FPLean/HelloWorld/StepByStep.lean | 16 ++++++++-------- book/FPLean/TypeClasses/Coercions.lean | 4 ++-- examples/Examples/Classes.lean | 4 ++-- examples/Examples/HelloWorld.lean | 4 ++-- examples/hello-name/HelloName.lean | 6 +++--- 6 files changed, 20 insertions(+), 20 deletions(-) diff --git a/book/FPLean/HelloWorld/RunningAProgram.lean b/book/FPLean/HelloWorld/RunningAProgram.lean index eb95bea..de3a55c 100644 --- a/book/FPLean/HelloWorld/RunningAProgram.lean +++ b/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) diff --git a/book/FPLean/HelloWorld/StepByStep.lean b/book/FPLean/HelloWorld/StepByStep.lean index acd7429..f11b80f 100644 --- a/book/FPLean/HelloWorld/StepByStep.lean +++ b/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 diff --git a/book/FPLean/TypeClasses/Coercions.lean b/book/FPLean/TypeClasses/Coercions.lean index 892c8c8..dc197f6 100644 --- a/book/FPLean/TypeClasses/Coercions.lean +++ b/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`. diff --git a/examples/Examples/Classes.lean b/examples/Examples/Classes.lean index d11dd78..8a03a42 100644 --- a/examples/Examples/Classes.lean +++ b/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 diff --git a/examples/Examples/HelloWorld.lean b/examples/Examples/HelloWorld.lean index c9291da..426d918 100644 --- a/examples/Examples/HelloWorld.lean +++ b/examples/Examples/HelloWorld.lean @@ -19,7 +19,7 @@ stop discarding -/ #check_msgs in -- ANCHOR: dropBang -#eval "Hello!!!".dropRightWhile (· == '!') +#eval "Hello!!!".dropEndWhile (· == '!') -- ANCHOR_END: dropBang /-- info: @@ -27,7 +27,7 @@ stop discarding -/ #check_msgs in -- ANCHOR: dropNonLetter -#eval "Hello... ".dropRightWhile (fun c => not (c.isAlphanum)) +#eval "Hello... ".dropEndWhile (fun c => not (c.isAlphanum)) -- ANCHOR_END: dropNonLetter diff --git a/examples/hello-name/HelloName.lean b/examples/hello-name/HelloName.lean index 02fcb7f..dbe68a0 100644 --- a/examples/hello-name/HelloName.lean +++ b/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