@[irreducible]

def String.Slice.posGE (s : Slice) (offset : Pos.Raw) (h : offset ≤ s.rawEndPos) : s.Pos

Obtains the smallest valid position that is greater than or equal to the given byte position.

@[inline]

def String.Slice.posGT (s : Slice) (offset : Pos.Raw) (h : offset < s.rawEndPos) : s.Pos

Obtains the smallest valid position that is strictly greater than the given byte position.

@[deprecated String.Slice.posGT (since := "2026-02-03")]

def String.Slice.findNextPos (offset : Pos.Raw) (s : Slice) (h : offset < s.rawEndPos) : s.Pos

@[inline]

def String.posGE (s : String) (offset : Pos.Raw) (h : offset ≤ s.rawEndPos) : s.Pos

Obtains the smallest valid position that is greater than or equal to the given byte position.

@[inline]

def String.posGT (s : String) (offset : Pos.Raw) (h : offset < s.rawEndPos) : s.Pos

Obtains the smallest valid position that is strictly greater than the given byte position.

@[irreducible]

def String.Slice.posLE (s : Slice) (offset : Pos.Raw) : s.Pos

Obtains the largest valid position that is less than or equal to the given byte position.

@[inline]

def String.Slice.posLT (s : Slice) (offset : Pos.Raw) (_h : 0 < offset) : s.Pos

Obtains the largest valid position that is strictly less than the given byte position.

@[inline]

def String.posLE (s : String) (offset : Pos.Raw) : s.Pos

Obtains the largest valid position that is less than or equal to the given byte position.

@[inline]

def String.posLT (s : String) (offset : Pos.Raw) (h : 0 < offset) : s.Pos

Obtains the largest valid position that is strictly less than the given byte position.

@[inline]

def String.Slice.Pos.prev {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos

Returns the previous valid position before the given position, given a proof that the position is not the start position, which guarantees that such a position exists.

def String.Slice.Pos.prev? {s : Slice} (pos : s.Pos) : Option s.Pos

Returns the previous valid position before the given position, or none if the position is the start position.

def String.Slice.Pos.prev! {s : Slice} (pos : s.Pos) : s.Pos

Returns the previous valid position before the given position, or panics if the position is the start position.

@[inline]

def String.Pos.prev {s : String} (pos : s.Pos) (h : pos ≠ s.startPos) : s.Pos

Returns the previous valid position before the given position, given a proof that the position is not the start position, which guarantees that such a position exists.

@[inline]

def String.Pos.prev? {s : String} (pos : s.Pos) : Option s.Pos

Returns the previous valid position before the given position, or none if the position is the start position.

@[inline]

def String.Pos.prev! {s : String} (pos : s.Pos) : s.Pos

Returns the previous valid position before the given position, or panics if the position is the start position.

def String.Slice.Pos.prevn {s : Slice} (p : s.Pos) (n : Nat) : s.Pos

Iterates p.prev n times.

If this would move p past the start of s, the result is s.endPos.

@[inline]

def String.Pos.prevn {s : String} (p : s.Pos) (n : Nat) : s.Pos

Iterates p.prev n times.

If this would move p past the start of s, the result is s.startPos.