From 1631326887adeb9c7bf08e437ded799525d167dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Tue, 23 Jan 2024 19:46:21 +0900 Subject: [PATCH] Update src/Idris/Error.idr --- src/Idris/Error.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index a20be6fce..f26c6dc49 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -644,7 +644,7 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi spellingCandidates = case candidates of [] => [] [x] => ["Did you mean" <++> enclose "'" "'" (pretty0 x) <++> "?"] - xs => ["Did you mean one of:" <++> hcat (punctuate ", " + xs => ["Did you mean either of:" <++> hcat (punctuate ", " (map (enclose "'" "'" . pretty0) xs)) <++> "?"]