@[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.

Equations

• s.posGE offset h = if h' : String.Pos.Raw.IsValidForSlice s offset then s.pos offset h' else have this := ⋯; s.posGE offset.inc ⋯

@[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.

Equations

• s.posGT offset h = s.posGE offset.inc ⋯

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

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

Equations

• String.Slice.findNextPos offset s h = s.posGT offset h

@[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.

Equations

• s.posGE offset h = String.Pos.ofToSlice (s.toSlice.posGE offset ⋯)

@[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.

Equations

• s.posGT offset h = String.Pos.ofToSlice (s.toSlice.posGT offset ⋯)

@[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.

Equations

• s.posLE offset = if h' : String.Pos.Raw.IsValidForSlice s offset then s.pos offset h' else have this := ⋯; s.posLE offset.dec

@[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.

Equations

• s.posLT offset _h = s.posLE offset.dec

@[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.

Equations

• s.posLE offset = String.Pos.ofToSlice (s.toSlice.posLE offset)

@[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.

Equations

• s.posLT offset h = String.Pos.ofToSlice (s.toSlice.posLT offset h)

@[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.

Equations

• pos.prev h = s.posLT pos.offset ⋯

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.

Equations

• pos.prev? = if h : pos = s.startPos then none else some (pos.prev h)

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.

Equations

• pos.prev! = if h : pos = s.startPos then panicWithPosWithDecl "Init.Data.String.FindPos" "String.Slice.Pos.prev!" 115 31 "The start position has no previous position" else pos.prev h

@[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.

Equations

• pos.prev h = String.Pos.ofToSlice (pos.toSlice.prev ⋯)

@[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.

Equations

• pos.prev? = Option.map String.Pos.ofToSlice pos.toSlice.prev?

@[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.

Equations

• pos.prev! = String.Pos.ofToSlice pos.toSlice.prev!

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.

Equations

• p.prevn 0 = p
• p.prevn n_2.succ = if h : p ≠ s.startPos then (p.prev h).prevn n_2 else p

@[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.

Equations

• p.prevn n = String.Pos.ofToSlice (p.toSlice.prevn n)