Skip to content

Commit 188ef68

Browse files
authored
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.
1 parent 5fd8c1b commit 188ef68

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Elab/GuardMsgs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -200,7 +200,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
200200
match filterFn msg with
201201
| .check => toCheck := toCheck.add msg
202202
| .drop => pure ()
203-
| pass => toPassthrough := toPassthrough.add msg
203+
| .pass => toPassthrough := toPassthrough.add msg
204204
let map ← getFileMap
205205
let reportPos? :=
206206
if reportPositions then

0 commit comments

Comments
 (0)