Deprecated aliases can be dumped here if they are no longer used in Mathlib, to avoid needing their imports if they are otherwise unnecessary.

@[deprecated String.dropPrefix? (since := "2024-06-04")]

def String.getRest (s pre : String) : Option Substring

Alias of String.dropPrefix?.

---

If pre is a prefix of s, i.e. s = pre ++ t, returns the remainder t.

Equations

• String.getRest = String.dropPrefix?