@[irreducible]

def String.Slice.Model.positionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos }

A list of all positions starting at p.

This function is not meant to be used in actual progams. Actual programs should use Slice.positionsFrom or Slice.positions.

@[simp]

theorem String.Slice.Model.positionsFrom_endPos {s : Slice} : Model.positionsFrom s.endPos = []

theorem String.Slice.Model.positionsFrom_eq_cons {s : Slice} {p : s.Pos} (hp : p ≠ s.endPos) : Model.positionsFrom p = ⟨p, hp⟩ :: Model.positionsFrom (p.next hp)

theorem String.Slice.Model.map_get_positionsFrom_of_splits {s : Slice} {p : s.Pos} {t₁ t₂ : String} (hp : p.Splits t₁ t₂) : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom p) = t₂.toList

theorem String.Slice.Model.map_get_positionsFrom_startPos {s : Slice} : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom s.startPos) = s.copy.toList

@[simp]

theorem String.Slice.toList_positionsFrom {s : Slice} {p : s.Pos} : (positionsFrom p).toList = Model.positionsFrom p

@[simp]

theorem String.Slice.toList_positions {s : Slice} : s.positions.toList = Model.positionsFrom s.startPos

@[simp]

theorem String.Slice.toList_chars {s : Slice} : s.chars.toList = s.copy.toList

@[irreducible]

def String.Slice.Model.revPositionsFrom {s : Slice} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos }

A list of all positions strictly before p, ordered from largest to smallest.

This function is not meant to be used in actual programs. Actual programs should use Slice.revPositionsFrom and Slice.revPositions.

@[simp]

theorem String.Slice.Model.revPositionsFrom_startPos {s : Slice} : Model.revPositionsFrom s.startPos = []

theorem String.Slice.Model.revPositionsFrom_eq_cons {s : Slice} {p : s.Pos} (hp : p ≠ s.startPos) : Model.revPositionsFrom p = ⟨p.prev hp, ⋯⟩ :: Model.revPositionsFrom (p.prev hp)

theorem String.Slice.Model.map_get_revPositionsFrom_of_splits {s : Slice} {p : s.Pos} {t₁ t₂ : String} (hp : p.Splits t₁ t₂) : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.revPositionsFrom p) = t₁.toList.reverse

theorem String.Slice.Model.map_get_revPositionsFrom_endPos {s : Slice} : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.revPositionsFrom s.endPos) = s.copy.toList.reverse

@[simp]

theorem String.Slice.toList_revPositionsFrom {s : Slice} {p : s.Pos} : (s.revPositionsFrom p).toList = Model.revPositionsFrom p

@[simp]

theorem String.Slice.toList_revPositions {s : Slice} : s.revPositions.toList = Model.revPositionsFrom s.endPos

@[simp]

theorem String.Slice.toList_revChars {s : Slice} : s.revChars.toList = s.copy.toList.reverse

theorem String.Slice.forIn_eq_forIn_chars {β : Type u} {m : Type u → Type v} [Monad m] {s : Slice} {b : β} {f : Char → β → m (ForInStep β)} : forIn s b f = forIn s.chars b f

@[simp]

theorem String.Slice.forIn_eq_forIn_toList {β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : Slice} {b : β} {f : Char → β → m (ForInStep β)} : forIn s b f = forIn s.copy.toList b f

@[irreducible]

def String.Model.positionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos }

A list of all positions starting at p.

This function is not meant to be used in actual progams. Actual programs should use Slice.positionsFrom or Slice.positions.

@[simp]

theorem String.Model.positionsFrom_endPos {s : String} : Model.positionsFrom s.endPos = []

theorem String.Model.positionsFrom_eq_cons {s : String} {p : s.Pos} (hp : p ≠ s.endPos) : Model.positionsFrom p = ⟨p, hp⟩ :: Model.positionsFrom (p.next hp)

theorem String.Model.positionsFrom_eq_map {s : String} {p : s.Pos} : Model.positionsFrom p = List.map (fun (p : { p : s.toSlice.Pos // p ≠ s.toSlice.endPos }) => ⟨Pos.ofToSlice p.val, ⋯⟩) (Slice.Model.positionsFrom p.toSlice)

theorem String.Model.map_get_positionsFrom_of_splits {s : String} {p : s.Pos} {t₁ t₂ : String} (hp : p.Splits t₁ t₂) : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom p) = t₂.toList

theorem String.Model.map_get_positionsFrom_startPos {s : String} : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.positionsFrom s.startPos) = s.toList

@[simp]

theorem String.toList_positionsFrom {s : String} {p : s.Pos} : (s.positionsFrom p).toList = Model.positionsFrom p

theorem String.toList_positions {s : String} : s.positions.toList = Model.positionsFrom s.startPos

@[simp]

theorem String.toList_chars {s : String} : s.chars.toList = s.toList

@[irreducible]

def String.Model.revPositionsFrom {s : String} (p : s.Pos) : List { p : s.Pos // p ≠ s.endPos }

A list of all positions strictly before p, ordered from largest to smallest.

This function is not meant to be used in actual programs. Actual programs should use Slice.revPositionsFrom and Slice.revPositions.

@[simp]

theorem String.Model.revPositionsFrom_startPos {s : String} : Model.revPositionsFrom s.startPos = []

theorem String.Model.revPositionsFrom_eq_cons {s : String} {p : s.Pos} (hp : p ≠ s.startPos) : Model.revPositionsFrom p = ⟨p.prev hp, ⋯⟩ :: Model.revPositionsFrom (p.prev hp)

theorem String.Model.revPositionsFrom_eq_map {s : String} {p : s.Pos} : Model.revPositionsFrom p = List.map (fun (p : { p : s.toSlice.Pos // p ≠ s.toSlice.endPos }) => ⟨Pos.ofToSlice p.val, ⋯⟩) (Slice.Model.revPositionsFrom p.toSlice)

theorem String.Model.map_get_revPositionsFrom_of_splits {s : String} {p : s.Pos} {t₁ t₂ : String} (hp : p.Splits t₁ t₂) : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.revPositionsFrom p) = t₁.toList.reverse

theorem String.Model.map_get_revPositionsFrom_endPos {s : String} : List.map (fun (p : { p : s.Pos // p ≠ s.endPos }) => p.val.get ⋯) (Model.revPositionsFrom s.endPos) = s.toList.reverse

@[simp]

theorem String.toList_revPositionsFrom {s : String} {p : s.Pos} : (s.revPositionsFrom p).toList = Model.revPositionsFrom p

@[simp]

theorem String.toList_revPositions {s : String} : s.revPositions.toList = Model.revPositionsFrom s.endPos

@[simp]

theorem String.toList_revChars {s : String} : s.revChars.toList = s.toList.reverse

theorem String.forIn_eq_forIn_chars {β : Type u} {m : Type u → Type v} [Monad m] {s : String} {b : β} {f : Char → β → m (ForInStep β)} : forIn s b f = forIn s.chars b f

@[simp]

theorem String.forIn_eq_forIn_toList {β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : String} {b : β} {f : Char → β → m (ForInStep β)} : forIn s b f = forIn s.toList b f