String.isSuffixOf

Stream: mathlib4

[David Renshaw]

String.isSuffixOf was removed in https://github.com/leanprover-community/mathlib4/pull/5409.
(It was in Mathlib/Data/String/Defs.lean.)

Is there an intended replacement? I don't see anything in std4 or core.

[David Renshaw]

I ended up using List.isSuffixOf on the data field of String. https://github.com/dwrensha/math-puzzles-in-lean4/blob/ee35295f93c619df195541bdde7e603518984803/scripts/buildWebpage.lean#L18

[Scott Morrison]

I think this was a mistake. There is String.dropSuffix which returns an Option, which you can then convert to a Bool via isSome.