ink

def Substring.dropPrefix? (s : Substring) (pre : Substring) : Option Substring

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

Equations

• Substring.dropPrefix? s pre = Substring.dropPrefix?.go s pre 0 (pre.stopPos - pre.startPos)

ink

def Substring.dropPrefix?.go (s : Substring) (pre : Substring) (start : String.Pos) (stop : String.Pos) : Option Substring

Auxiliary definition for dropPrefix?.

Equations

• One or more equations did not get rendered due to their size.

ink

def String.dropPrefix? (s : String) (pre : String) : Option Substring

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

Equations

• String.dropPrefix? s pre = Substring.dropPrefix? (String.toSubstring s) (String.toSubstring pre)