compare — Mathlib

Lean4
/-- Determine whether a `new` `ErrorContext` is covered by an `existing` exception,
and, if it is, if we prefer replacing the new exception or keeping the previous one. -/
def compare (existing new : ErrorContext) : ComparisonResult :=
  -- Two comparable error contexts must have the same path.
    -- To avoid issues with different path separators across different operating systems,
    -- we compare the set of path components instead.

  if existing.path.components != new.path.components then ComparisonResult.Different
  else if existing.error == new.error then ComparisonResult.Comparable else ComparisonResult.Different
Похожие утверждения