diff --git a/Parser/Basic.lean b/Parser/Basic.lean
index ddee1c3f..21cc56ab 100644
--- a/Parser/Basic.lean
+++ b/Parser/Basic.lean
@@ -12,7 +12,7 @@ public import Parser.Stream
 public section
 
 namespace Parser
-variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]
+variable {σ τ} [Parser.Stream σ τ] {ε} [Parser.Error ε σ τ] {m} [Monad m]
 
 /-! # Token Functions -/
 
@@ -22,10 +22,11 @@ variable [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m]
 This is a low-level parser to customize how the parser stream is used.
 -/
 @[inline]
-def tokenCore (next? : σ → Option (τ × σ)) : ParserT ε σ τ m τ := do
-  match next? (← getStream) with
-  | some (tok, stream) =>
-    let _ ← setStream stream
+def tokenCore (next? : Stream.Position σ → Option (τ × Stream.Position σ)) :
+    ParserT ε σ τ m τ := do
+  match next? (← getPosition) with
+  | some (tok, pos) =>
+    setPosition pos
     return tok
   | none => throwUnexpected
 
@@ -35,7 +36,7 @@ the unexpected token.
 -/
 @[specialize]
 def tokenMap (test : τ → Option α) : ParserT ε σ τ m α := do
-  let tok ← tokenCore Stream.next?
+  let tok ← tokenCore (Stream.next? (← getStream))
   match test tok with
   | some x => return x
   | none => throwUnexpected tok
diff --git a/Parser/Char/Basic.lean b/Parser/Char/Basic.lean
index bdba2ebf..bb4d4f5c 100644
--- a/Parser/Char/Basic.lean
+++ b/Parser/Char/Basic.lean
@@ -26,15 +26,18 @@ def chars (tks : String) : ParserT ε σ Char m String :=
     return acc
 
 /-- `string tks` accepts and returns string `tks`, otherwise fails -/
-def string [Parser.Error ε String.Slice Char] (tks : String.Slice) :
-    ParserT ε String.Slice Char m String.Slice :=
-  withErrorMessage s!"expected {repr tks.toString}" do
-    match (← getStream).dropPrefix? tks with
-    | some s =>
-      setStream s
-      return tks
-    | none =>
-      throwUnexpected
+def string [Parser.Error ε String.Slice Char] (tks : String) :
+    ParserT ε String.Slice Char m String :=
+  withErrorMessage s!"expected {repr tks}" do
+    let s ← getStream
+    let pos ← getPosition
+    if h : pos.IsValidForSlice s then
+      match (s.sliceFrom ⟨pos, h⟩).skipPrefix? tks with
+      | some ⟨pos', _⟩ =>
+        setPosition pos'
+        return tks
+      | none => throwUnexpected
+    else throwUnexpected
 
 /-- `captureStr p` parses `p` and returns the output of `p` with the corresponding `String.Slice` -/
 def captureStr {α} [h : Parser.Error ε String.Slice Char] (p : ParserT ε String.Slice Char m α) :
@@ -46,7 +49,7 @@ def captureStr {α} [h : Parser.Error ε String.Slice Char] (p : ParserT ε Stri
     return (x, ⟨s.str, ⟨start, h'.1⟩ , ⟨stop, h'.2.1⟩, String.Pos.le_iff.1 h'.2.2⟩)
   else
     have : Inhabited (ParserT ε String.Slice Char m (α × String.Slice)) :=
-      ⟨fun s => return .error s (h.unexpected 0 none)⟩
+      ⟨fun s pos => return .error s pos (h.unexpected 0 none)⟩
     unreachable!
 
 /--
diff --git a/Parser/Error.lean b/Parser/Error.lean
index 39961974..f5a4f0c9 100644
--- a/Parser/Error.lean
+++ b/Parser/Error.lean
@@ -63,13 +63,13 @@ This error type records the position and, optionally, the offending token where
 occurred; any additional information is discarded. This is useful for parsers where the cause of
 parsing errors is predictable and only the position of the error is needed for processing.
 -/
-abbrev Basic (σ τ) [Parser.Stream σ τ] := Parser.Stream.Position σ × Option τ
+abbrev Basic (σ τ) [Parser.Stream σ τ] := Stream.Position σ × Option τ
 
 instance (σ τ) [Parser.Stream σ τ] : Parser.Error (Basic σ τ) σ τ where
   unexpected p t := (p, t)
   addMessage e _ _ := e
 
-instance (σ τ) [Repr τ] [Parser.Stream σ τ] [Repr (Parser.Stream.Position σ)] :
+instance (σ τ) [Repr τ] [Parser.Stream σ τ] [Repr (Stream.Position σ)] :
   ToString (Basic σ τ) where
   toString
     | (pos, some tok) => s!"unexpected input {repr tok} at {repr pos}"
@@ -87,8 +87,8 @@ inductive Simple (σ τ) [Parser.Stream σ τ]
   | addMessage : Simple σ τ → Stream.Position σ → String → Simple σ τ
 
 -- The derive handler for `Repr` fails, this is a workaround.
-protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ] [Repr (Stream.Position σ)] :
-  Simple σ τ → Nat → Std.Format
+protected def Simple.reprPrec {σ τ} [Parser.Stream σ τ] [Repr τ]
+    [Repr (Stream.Position σ)] : Simple σ τ → Nat → Std.Format
   | unexpected pos a, prec =>
     Repr.addAppParen
       (Std.Format.group
diff --git a/Parser/Parser.lean b/Parser/Parser.lean
index db980558..a5adc6b3 100644
--- a/Parser/Parser.lean
+++ b/Parser/Parser.lean
@@ -11,12 +11,12 @@ public import Parser.Stream
 public section
 
 /-- Parser result type. -/
-protected inductive Parser.Result (ε σ α : Type _) : Type u
+protected inductive Parser.Result {τ} (ε σ α : Type u) [Parser.Stream σ τ] : Type u
   /-- Result: success! -/
-  | ok : σ → α → Parser.Result ε σ α
+  | ok : σ → Parser.Stream.Position σ → α → Parser.Result ε σ α
   /-- Result: error! -/
-  | error : σ → ε → Parser.Result ε σ α
-  deriving Inhabited, Repr
+  | error : σ → Parser.Stream.Position σ → ε → Parser.Result ε σ α
+deriving Inhabited -- TODO : manually implement Repr
 
 /--
 `ParserT ε σ τ` is a monad transformer to parse tokens of type `τ` from the stream type `σ` with
@@ -24,56 +24,55 @@ error type `ε`.
 -/
 @[expose]
 def ParserT (ε σ τ : Type _) [Parser.Stream σ τ] [Parser.Error ε σ τ] (m : Type _ → Type _)
-  (α : Type _) : Type _ := σ → m (Parser.Result ε σ α)
+  (α : Type _) : Type _ := σ → Parser.Stream.Position σ → m (Parser.Result ε σ α)
 
 /-- Run the monadic parser `p` on input stream `s`. -/
 @[inline]
-def ParserT.run [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : ParserT ε σ τ m α) (s : σ) :
-  m (Parser.Result ε σ α) := p s
+def ParserT.run [stream : Parser.Stream σ τ] [Parser.Error ε σ τ]
+    (p : ParserT ε σ τ m α) (s : σ) (pos : optParam stream.Position (stream.start s)):
+  m (Parser.Result ε σ α) := p s pos
 
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   Monad (ParserT ε σ τ m) where
-  pure x s := return .ok s x
-  bind x f s := x s >>= fun
-    | .ok s a => f a s
-    | .error s e => return .error s e
-  map f x s := x s >>= fun
-    | .ok s a => return .ok s (f a)
-    | .error s e => return .error s e
-  seq f x s := f s >>= fun
-    | .ok s f => x () s >>= fun
-      | .ok s x => return .ok s (f x)
-      | .error s e => return .error s e
-    | .error s e => return .error s e
-  seqLeft x y s := x s >>= fun
-    | .ok s x => y () s >>= fun
-      | .ok s _ => return .ok s x
-      | .error s e => return .error s e
-    | .error s e => return .error s e
-  seqRight x y s := x s >>= fun
-    | .ok s _ => y () s >>= fun
-      | .ok s y => return .ok s y
-      | .error s e => return .error s e
-    | .error s e => return .error s e
+  pure x s pos := return .ok s pos x
+  bind x f s pos := x s pos >>= fun
+    | .ok s pos a => f a s pos
+    | .error s pos e => return .error s pos e
+  map f x s pos := x s pos >>= fun
+    | .ok s pos a => return .ok s pos (f a)
+    | .error s pos e => return .error s pos e
+  seq f x s pos := f s pos >>= fun
+    | .ok s pos f => x () s pos >>= fun
+      | .ok s pos x => return .ok s pos (f x)
+      | .error s pos e => return .error s pos e
+    | .error s pos e => return .error s pos e
+  seqLeft x y s pos := x s pos >>= fun
+    | .ok s pos x => y () s pos >>= fun
+      | .ok s pos _ => return .ok s pos x
+      | .error s pos e => return .error s pos e
+    | .error s pos e => return .error s pos e
+  seqRight x y s pos := x s pos >>= fun
+    | .ok s pos _ => y () s pos >>= fun
+      | .ok s pos y => return .ok s pos y
+      | .error s pos e => return .error s pos e
+    | .error s pos e => return .error s pos e
 
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   MonadExceptOf ε (ParserT ε σ τ m) where
-  throw e s := return .error s e
-  tryCatch p c s := p s >>= fun
-    | .ok s v => return .ok s v
-    | .error s e => (c e).run s
+  throw e s pos := return .error s pos e
+  tryCatch p c s pos := p s pos >>= fun
+    | .ok s pos v => return .ok s pos v
+    | .error s pos e => (c e).run s pos
 
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   OrElse (ParserT ε σ τ m α) where
-  orElse p q s :=
-    let savePos := Parser.Stream.getPosition s
-    p s >>= fun
-    | .ok s v => return .ok s v
-    | .error s _ => q () (Parser.Stream.setPosition s savePos)
-
+  orElse p q s pos :=
+    p s pos >>= fun
+    | .ok s pos v => return .ok s pos v
+    | .error s _ _ => q () s pos
 instance (σ ε τ m) [Parser.Stream σ τ] [Parser.Error ε σ τ] [Monad m] :
   MonadLift m (ParserT ε σ τ m) where
-  monadLift x s := (.ok s ·) <$> x
+  monadLift x s pos := (.ok s pos ·) <$> x
 
 /--
 `Parser ε σ τ` monad to parse tokens of type `τ` from the stream type `σ` with error type `ε`.
@@ -83,7 +82,7 @@ abbrev Parser (ε σ τ) [Parser.Stream σ τ] [Parser.Error ε σ τ] := Parser
 /-- Run parser `p` on input stream `s`. -/
 @[inline]
 protected def Parser.run {ε σ τ α} [Parser.Stream σ τ] [Parser.Error ε σ τ] (p : Parser ε σ τ α)
-  (s : σ) : Parser.Result ε σ α := p s
+  (s : σ) : Parser.Result ε σ α := p s (Stream.start s)
 
 /--
 `TrivialParserT σ τ` monad transformer to parse tokens of type `τ` from the stream `σ` with trivial
@@ -127,22 +126,17 @@ variable {ε σ α β : Type u} [Parser.Stream σ τ] [Parser.Error ε σ τ] [M
 /-- Get parser stream. -/
 @[inline]
 def getStream : ParserT ε σ τ m σ :=
-  fun s => return .ok s s
-
-/-- Set parser stream. -/
-@[inline]
-def setStream (s : σ) : ParserT ε σ τ m PUnit :=
-  fun _ => return .ok s PUnit.unit
+  fun s pos => return .ok s pos s
 
 /-- Get stream position from parser. -/
 @[inline]
 def getPosition : ParserT ε σ τ m (Stream.Position σ) :=
-  Stream.getPosition <$> getStream
+  fun s pos => return .ok s pos pos
 
 /-- Set stream position from parser. -/
 @[inline]
 def setPosition (pos : Stream.Position σ) : ParserT ε σ τ m PUnit := do
-  setStream <| Stream.setPosition (← getStream) pos
+  fun s _ => return .ok s pos PUnit.unit
 
 /-- `withBacktracking p` parses `p` but does not consume any input on error. -/
 @[inline]
@@ -191,14 +185,13 @@ def withErrorMessage (msg : String) (p : ParserT ε σ τ m α) : ParserT ε σ
 
 @[specialize]
 private partial def efoldlPAux [Inhabited ε] [Inhabited σ] [Inhabited β]
-  (f : β → α → ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (y : β) (s : σ) :
-  m (Parser.Result ε σ (β × ε × Bool)) :=
-  let savePos := Stream.getPosition s
-  p s >>= fun
-    | .ok s x => f y x s >>= fun
-      | .ok s y => efoldlPAux f p y s
-      | .error s e => return .ok (Stream.setPosition s savePos) (y, e, true)
-    | .error s e => return .ok (Stream.setPosition s savePos) (y, e, false)
+    (f : β → α → ParserT ε σ τ m β) (p : ParserT ε σ τ m α) (y : β) (s : σ)
+    (pos : Stream.Position σ ) : m (Parser.Result ε σ (β × ε × Bool)) :=
+  p s pos >>= fun
+    | .ok s pos' x => f y x s pos' >>= fun
+      | .ok s pos' y => efoldlPAux f p y s pos'
+      | .error s _ e => return .ok s pos (y, e, true)
+    | .error s _ e => return .ok s pos (y, e, false)
 
 /--
 `foldlP f init p` folds the parser function `f` from left to right using `init` as an intitial
@@ -216,7 +209,7 @@ def efoldlP (f : β → α → ParserT ε σ τ m β) (init : β) (p : ParserT 
   fun s =>
     have : Inhabited β := ⟨init⟩
     have : Inhabited σ := ⟨s⟩
-    have : Inhabited ε := ⟨Error.unexpected (Stream.getPosition s) none⟩
+    have : Inhabited ε := ⟨Error.unexpected (Stream.start s) none⟩
     efoldlPAux f p init s
 
 /--
@@ -276,11 +269,10 @@ This parser never fails.
 -/
 @[specialize]
 def eoption (p : ParserT ε σ τ m α) : ParserT ε σ τ m (Sum α ε) :=
-  fun s =>
-    let savePos := Stream.getPosition s
-    p s >>= fun
-    | .ok s x => return .ok s (.inl x)
-    | .error s e => return .ok (Stream.setPosition s savePos) (.inr e)
+  fun s pos =>
+    p s pos >>= fun
+    | .ok s pos x => return .ok s pos (.inl x)
+    | .error s _ e => return .ok s pos (.inr e)
 
 /--
 `optionM p` tries to parse `p` (with backtracking) and returns `x` if `p` returns `x`, returns the
@@ -357,11 +349,9 @@ def first (ps : List (ParserT ε σ τ m α)) (combine : ε → ε → ε := fun
   go ps (Error.unexpected (← getPosition) none)
 where
   go : List (ParserT ε σ τ m α) → ε → ParserT ε σ τ m α
-    | [], e, s => return .error s e
-    | p :: ps, e, s =>
-      let savePos := Stream.getPosition s
-      p s >>= fun
-      | .ok s v => return .ok s v
-      | .error s f => go ps (combine e f) (Stream.setPosition s savePos)
-
+    | [], e, s, pos => return .error s pos e
+    | p :: ps, e, s, pos =>
+      p s pos >>= fun
+      | .ok s pos v => return .ok s pos v
+      | .error s _ f => go ps (combine e f) s pos
 end Parser
diff --git a/Parser/RegEx/Compile.lean b/Parser/RegEx/Compile.lean
index 6634db2e..8fe9e4e0 100644
--- a/Parser/RegEx/Compile.lean
+++ b/Parser/RegEx/Compile.lean
@@ -171,8 +171,8 @@ end
 /-- Compiles a regex from a string, returns `none` on faiure -/
 protected def compile? (s : String) : Option (RegEx Char) :=
   match Parser.run (re0 <* endOfInput) s with
-  | .ok _ r => some r
-  | .error _ _ => none
+  | .ok _ _ r => some r
+  | .error _ _ _ => none
 
 /-- Compiles a regex from a string, panics on faiure -/
 protected def compile! (s : String) : RegEx Char :=
diff --git a/Parser/Stream.lean b/Parser/Stream.lean
index cc05b533..996831f6 100644
--- a/Parser/Stream.lean
+++ b/Parser/Stream.lean
@@ -10,49 +10,40 @@ public section
 
 /-! # Parser Stream
 
-Parsers read input tokens from a stream. To help with error reporting and backtracking, the
-`Parser.Stream` class extends the basic `Stream` class with functionality to save and restore
-stream positions.
-
-The simple way to implement backtracking after a parsing error is to first save the stream state
-before parsing and, upon encountering an error, restore the saved stream state. The issue with this
-strategy is that each backtrack point adds a reference to the entire stream state. This prevents
-linear use of the stream state. The `Parser.Stream` class allows users to work around this issue.
-The `Parser.Stream.Position` type is intended to store just enough information to *reconstruct* the
-stream state at a save point without having to save the entire stream state.
+Parsers read input tokens from a stream. In contrast to the `Std.Stream` class, the stream itself
+does not change, but instead we keep track of the position inside the stream. This helps with
+error reporting and and allows for backtracking.
 -/
 
 /-- *Parser stream class*
 
-This class extends the basic `Stream` class with position features needed by parsers for
-backtracking and error reporting.
+This class implements streams based on a static stream with a moving position.
 
 * The type `Position` is used to record position data for the stream type.
-* `getPosition (s : σ) : Position` returns the current position of stream `s`.
-* `setPosition (s : σ) (p : Position) : σ` restores stream `s` to position `p`.
+* `start (s : σ) : Position` returns starting position for the stream `s`
+* `next? (s : σ) (pos : Position) : Option (τ × Position)` returns the token at position `pos` in
+  `s` together with the next position. It returns `none` if the end of the stream has been reached.
 
-Implementations should try to make the `Position` type as lightweight as possible for `getPosition`
-and `setPosition` to work properly. Often `Position` is just a scalar type or another simple type.
+Implementations should try to make the `Position` type as lightweight as possible. Often `Position`
+is just a scalar type or another simple type.
 This may allow for parsers to use the stream state more efficiently.
 -/
-protected class Parser.Stream.{u_1} (σ : Type _) (τ : outParam (Type _)) extends Std.Stream σ τ where
-  Position : Type u_1
-  getPosition : σ → Position
-  setPosition : σ → Position → σ
+
+protected class Parser.Stream (σ : Type _) (τ : outParam (Type _)) where
+  Position : Type u
+  start : σ → Position
+  next? : σ →  Position → Option (τ × Position)
 attribute [reducible, inherit_doc Parser.Stream] Parser.Stream.Position
-attribute [inherit_doc Parser.Stream] Parser.Stream.getPosition Parser.Stream.setPosition
+attribute [inherit_doc Parser.Stream] Parser.Stream.start Parser.Stream.next?
+
+instance {σ τ} [self : Parser.Stream σ τ] [Inhabited σ] : Inhabited self.Position where
+  default := Parser.Stream.start default
 
 namespace Parser.Stream
 
 /-- Stream segment type. -/
 @[expose]
-def Segment (σ) [Parser.Stream σ τ] := Stream.Position σ × Stream.Position σ
-
-/-- Start position of stream segment. -/
-abbrev Segment.start [Parser.Stream σ τ] (s : Segment σ) := s.1
-
-/-- Stop position of stream segment. -/
-abbrev Segment.stop [Parser.Stream σ τ] (s : Segment σ) := s.2
+def Segment σ {τ} [self : Parser.Stream σ τ] := self.Position × self.Position
 
 /-- Default wrapper to make a `Parser.Stream` from a plain `Stream`.
 
@@ -64,82 +55,58 @@ def mkDefault (σ τ) [Std.Stream σ τ] := σ
 
 @[reducible]
 instance (σ τ) [self : Std.Stream σ τ] : Parser.Stream (mkDefault σ τ) τ where
-  toStream := self
   Position := σ
-  getPosition s := s
-  setPosition _ p := p
+  start s := s
+  next? _ := self.next?
+
+@[reducible]
+instance : Parser.Stream String Char where
+  Position := String.Pos.Raw
+  start s := s.rawStartPos
+  next? s p :=
+    if h : p.IsValid s ∧ p < s.rawEndPos then
+      some (String.Pos.get ⟨p, h.1⟩ (String.Pos.offset_lt_rawEndPos_iff.1 h.2) , p.next s)
+    else
+      none
+
 
 @[reducible]
 instance : Parser.Stream String.Slice Char where
   Position := String.Pos.Raw
-  getPosition s := s.startInclusive.offset
-  setPosition s p :=
-    if h : p.IsValid s.str then
-      s.str.slice! ⟨p, h⟩ s.endExclusive
+  start s := s.startPos.offset
+  next? s p :=
+    if h : p.IsValidForSlice s ∧ p < s.rawEndPos then
+      have h' : ⟨p, h.1⟩ ≠ s.endPos := String.Slice.Pos.offset_lt_rawEndPos_iff.1 h.2
+      some (String.Slice.Pos.get ⟨p, h.1⟩ h' , p.next s.str)
     else
-      panic! "invalid position for string"
+      none
 
+-- Substring.Raw is a legacy function, so maybe this should be removed.
 @[reducible]
 instance : Parser.Stream Substring.Raw Char where
   Position := String.Pos.Raw
-  getPosition s := s.startPos
-  setPosition s p :=
-    if p ≤ s.stopPos then
-      { s with startPos := p }
+  start s := s.startPos
+  next? s p :=  if p < s.stopPos then
+      some (s.startPos.get s.str, p.next s.str)
     else
-      { s with startPos := s.stopPos }
+      none
 
 @[reducible]
 instance (τ) : Parser.Stream (Subarray τ) τ where
   Position := Nat
-  getPosition s := s.start
-  setPosition s p :=
-    if h : p ≤ s.stop then
-      ⟨{ s.internalRepresentation with start := p, start_le_stop := h }⟩
-    else
-      ⟨{ s.internalRepresentation with start := s.stop, start_le_stop := Nat.le_refl s.stop }⟩
+  start s := s.start
+  next? s p := s[p]? >>= (· , p  + 1)
 
 @[reducible]
 instance : Parser.Stream ByteSlice UInt8 where
   Position := Nat
-  getPosition s := s.start
-  setPosition s p := s.byteArray.toByteSlice p s.stop
-
-/-- `OfList` is a view of a list stream that keeps track of consumed tokens. -/
-structure OfList (τ : Type _) where
-  /-- Remaining tokens. -/
-  next : List τ
-  /-- Consumed tokens. -/
-  past : List τ := []
-
-/-- Restore a list stream to a given position. -/
-def OfList.setPosition {τ} (s : OfList τ) (p : Nat) : OfList τ :=
-  if s.past.length < p then
-    fwd (p - s.past.length) s
-  else
-    rev (s.past.length - p) s
-where
-  /-- Internal for `OfList.setPosition`. -/
-  fwd : Nat → OfList τ → OfList τ
-    | k+1, ⟨x :: rest, past⟩ => fwd k ⟨rest, x :: past⟩
-    | _, s => s
-  /-- Internal for `OfList.setPosition`. -/
-  rev : Nat → OfList τ → OfList τ
-    | k+1, ⟨rest, x :: past⟩ => rev k ⟨x :: rest, past⟩
-    | _, s => s
-
-/-- Make a `Parser.Stream` from a `List`. -/
-def mkOfList {τ} (data : List τ) (pos : Nat := 0) : OfList τ :=
-  OfList.setPosition { next := data } pos
+  start s := s.start
+  next? s p := s[p]? >>= (· , p  + 1)
 
 @[reducible]
-instance (τ) : Parser.Stream (OfList τ) τ where
-  Position := Nat
-  getPosition s := s.past.length
-  setPosition := OfList.setPosition
-  next? s :=
-    match s with
-    | ⟨x :: rest, past⟩ => some (x, ⟨rest, x :: past⟩)
-    | _ => none
+instance (τ) : Parser.Stream (List τ) τ where
+  Position := List τ
+  start s := s
+  next? _ p := p.next?
 
 end Parser.Stream
diff --git a/examples/BNF.lean b/examples/BNF.lean
index 9ca15de9..e32aecf4 100644
--- a/examples/BNF.lean
+++ b/examples/BNF.lean
@@ -215,8 +215,8 @@ end BNFParser
 /-- Parse BNF from string -/
 def parse (input : String) : Except String BNF.Syntax :=
   match (BNFParser.syntax <* Parser.endOfInput).run input.toSlice with
-  | .ok _ stx => .ok stx
-  | .error _ err => .error ("error: " ++ toString err)
+  | .ok _ _ stx => .ok stx
+  | .error _ _ err => .error ("error: " ++ toString err)
 
 section Test
 
diff --git a/examples/JSON.lean b/examples/JSON.lean
index 7017a999..047480ab 100644
--- a/examples/JSON.lean
+++ b/examples/JSON.lean
@@ -205,7 +205,7 @@ end
 /-- JSON validator -/
 def validate (str : String) : Bool :=
   match Parser.run (ws *> JSON.value <* ws <* endOfInput) str.toSlice with
-  | .ok _ _ => true
-  | .error _ _ => false
+  | .ok _ _ _ => true
+  | .error _ _ _ => false
 
 end JSON
diff --git a/examples/Roman.lean b/examples/Roman.lean
index 1ef35291..1752ebbb 100644
--- a/examples/Roman.lean
+++ b/examples/Roman.lean
@@ -83,7 +83,7 @@ end Roman
 def String.toNatRoman? (s : String) (upper : Bool := true) : Option Nat :=
   let s := if upper then s else s.map .toUpper
   match Parser.run (Roman.parse <* Parser.endOfInput) s.toSlice with
-  | .ok _ (n+1) => some (n+1)
+  | .ok _ _ (n+1) => some (n+1)
   | _ => none
 
 @[inline, inherit_doc String.toNatRoman?]
diff --git a/test/issue-126.lean b/test/issue-126.lean
index 89508b8e..a81865ef 100644
--- a/test/issue-126.lean
+++ b/test/issue-126.lean
@@ -13,7 +13,7 @@ def test (tk : Char) : TestParser UInt8 := tokenFilter (· = tk.val.toUInt8)
 
 def run (p : TestParser UInt8) (input : String) : String :=
   let arr := input.toByteArray.toByteSlice
-  match p.run arr with | .ok _ x => s!"ok {Char.ofUInt8 x}" | .error _ e => s!"error {e}"
+  match p.run arr with | .ok _ _ x => s!"ok {Char.ofUInt8 x}" | .error _ _ e => s!"error {e}"
 
 /-- info: "ok a" -/
 #guard_msgs in #eval run (test 'a' <|> test 'b') "a"
diff --git a/test/issue-35.lean b/test/issue-35.lean
index bf95a50e..3d3877e4 100644
--- a/test/issue-35.lean
+++ b/test/issue-35.lean
@@ -4,7 +4,7 @@ open Parser
 
 def test : Bool :=
   match Parser.run (Char.string "abc" : SimpleParser String.Slice Char String) "abc" with
-  | .ok s r => s == "" && r == "abc"
-  | .error _ _ => false
+  | .ok s pos r => pos == s.rawEndPos && r == "abc"
+  | .error _ _ _ => false
 
 #guard test
diff --git a/test/issue-39.lean b/test/issue-39.lean
index b9456e73..23f5ef20 100644
--- a/test/issue-39.lean
+++ b/test/issue-39.lean
@@ -4,7 +4,7 @@ open Parser
 
 def test :=
   match (endOfInput : TrivialParser String.Slice Char Unit).run "abcd" with
-  | .ok _ _ => false
-  | .error _ _ => true
+  | .ok _ _ _ => false
+  | .error _ _ _ => true
 
 #guard test
diff --git a/test/readme-example.lean b/test/readme-example.lean
index e2f375ea..202fbd14 100644
--- a/test/readme-example.lean
+++ b/test/readme-example.lean
@@ -14,5 +14,5 @@ def parseSum : SimpleParser String.Slice Char Int := do
   return sum
 
 #guard 42 == match parseSum.run "11-1+2-3+33" with
-  | .ok _ sum => sum
-  | .error _ e => panic! (toString e)
+  | .ok _ _ sum => sum
+  | .error _ _ e => panic! (toString e)