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

Equations

• String.Slice.Model.positionsFrom p = if h : p.IsAtEnd then [] else ⟨p, h⟩ :: String.Slice.Model.positionsFrom (p.next h)

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

Equations

• String.Slice.Model.revPositionsFrom p = if h : p = s.startPos then [] else ⟨p.prev h, ⋯⟩ :: String.Slice.Model.revPositionsFrom (p.prev h)

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

Equations

• String.Model.positionsFrom p = if h : p.IsAtEnd then [] else ⟨p, h⟩ :: String.Model.positionsFrom (p.next h)

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

Equations

• String.Model.revPositionsFrom p = if h : p = s.startPos then [] else ⟨p.prev h, ⋯⟩ :: String.Model.revPositionsFrom (p.prev h)

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