From 188ef680da2d093b76162907867b816cd9d4e110 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Thu, 25 Sep 2025 14:50:46 +0100 Subject: [PATCH] chore: ensure `pass` refers to `SpecResult.pass` in GuardMsgs (#10539) This PR adds a `.` in front of `pass` in the `#guard_msgs` implementation. Previously, the match arm read `| pass => ...`. Presumably, `pass` was intended to mean `SpecResult.pass`, but, this isn't in scope, so instead `pass` here is a catch-all variable. By adding a dot, we ensure we actually refer to the constant. Note that this was the last case in the pattern-match, and since all other constructors were correctly referenced, the only case that went to the fallback was `SpecResult.pass`, so the code did the right thing. Still, by fixing this, we prevent a surprise in the event that a new `SpecResult` constructor is added. --- src/Lean/Elab/GuardMsgs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index e6acb2d14f..bb2d5a3a43 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/src/Lean/Elab/GuardMsgs.lean @@ -200,7 +200,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S match filterFn msg with | .check => toCheck := toCheck.add msg | .drop => pure () - | pass => toPassthrough := toPassthrough.add msg + | .pass => toPassthrough := toPassthrough.add msg let map ← getFileMap let reportPos? := if reportPositions then