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?]

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?