max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: change String.dropPrefix? signature (#5745)

Browse source
This commit is contained in:
Kim Morrison 2024-10-17 14:51:45 +11:00 • committed by GitHub
parent 69e8cd3d8a
commit e8970463d1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Init/Data/String/Basic.lean
View file

@ -1148,23 +1148,23 @@ namespace String
/--
If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
-/
def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
s.toSubstring.dropPrefix? pre
def dropPrefix? (s : String) (pre : String) : Option Substring :=
s.toSubstring.dropPrefix? pre.toSubstring
/--
If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
-/
def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
s.toSubstring.dropSuffix? suff
def dropSuffix? (s : String) (suff : String) : Option Substring :=
s.toSubstring.dropSuffix? suff.toSubstring
/-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
or otherwise return `s`. -/
def stripPrefix (s : String) (pre : Substring) : String :=
def stripPrefix (s : String) (pre : String) : String :=
s.dropPrefix? pre |>.map Substring.toString |>.getD s
/-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
or otherwise return `s`. -/
def stripSuffix (s : String) (suff : Substring) : String :=
def stripSuffix (s : String) (suff : String) : String :=
s.dropSuffix? suff |>.map Substring.toString |>.getD s
end String