pushFormatError — Mathlib

Lean4
/-- Add a new `FormatError` `f` to the array `fs`, trying, as much as possible, to merge the new
`FormatError` with the last entry of `fs`.
-/
def pushFormatError (fs : Array FormatError) (f : FormatError) : Array FormatError :=
  -- If there are no errors already, we simply add the new one.

  if fs.isEmpty then fs.push f
  else
    let back := fs.back!
    if back.msg != f.msg || back.srcNat - back.length != f.srcNat then fs.push f
    else
      -- Otherwise, we are adding a further error of the same kind and we therefore merge the two.
      fs.pop.push { back with length := back.length + f.length, srcStartPos := f.srcEndPos }
Похожие утверждения