From 7e1ee70b7ca69c13f5014a694879098594d390e0 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 21 Mar 2025 06:38:07 +0100 Subject: [PATCH] doc: add docstrings for String.drop and String.dropRight (#7607) This PR adds docstrings for `String.drop` and `String.dropRight`. --- src/Init/Data/String/Basic.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean index 8a81191235..0e5c053e59 100644 --- a/src/Init/Data/String/Basic.lean +++ b/src/Init/Data/String/Basic.lean @@ -1414,9 +1414,29 @@ end Substring namespace String +/-- +Removes the specified number of characters (Unicode code points) from the start of the string. + +If `n` is greater than `s.length`, returns `""`. + +Examples: + * `"red green blue".drop 4 = "green blue"` + * `"red green blue".drop 10 = "blue"` + * `"red green blue".drop 50 = ""` +-/ @[inline] def drop (s : String) (n : Nat) : String := (s.toSubstring.drop n).toString +/-- +Removes the specified number of characters (Unicode code points) from the end of the string. + +If `n` is greater than `s.length`, returns `""`. + +Examples: + * `"red green blue".dropRight 5 = "red green"` + * `"red green blue".dropRight 11 = "red"` + * `"red green blue".dropRight 50 = ""` +-/ @[inline] def dropRight (s : String) (n : Nat) : String := (s.toSubstring.dropRight n).toString