Possible bug in Lean/Parser/Basic.lean:setExpectedFn

Stream: lean4

[Richard L Ford]

I was reading the source of Lean 4 and ran into this function:

def setExpectedFn (expected : List String) (p : ParserFn) : ParserFn := fun c s =>
  match p c s with
    | s'@{ errorMsg := some msg, .. } => { s' with errorMsg := some { msg with expected := [] } }
    | s'                              => s'

I'm thinking it should be this instead:

def setExpectedFn (expected : List String) (p : ParserFn) : ParserFn := fun c s =>
  match p c s with
    | s'@{ errorMsg := some msg, .. } => { s' with errorMsg := some { msg with expected := expected} }
    | s'                              => s'

as the expected to the left of the ":=" is just telling the field of the Error structure that is to be changed.
Currently it appears that the "expected" parameter is not used.

I'm relatively new to Lean so thought I'd raise the issue here before taking any other action, like a pull request.

Thanks