From d75da06574444890e8ff1a86d4bacc6d9b52b997 Mon Sep 17 00:00:00 2001 From: Matthew Toohey Date: Sat, 17 Aug 2024 23:40:32 -0400 Subject: [PATCH] fix: correct typo in invalid reassignment error Corrects a small typo in the error message for when a user attempts to mutate something which cannot be mutated. --- src/Lean/Elab/Do.lean | 2 +- tests/lean/doNotation1.lean.expected.out | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index eb589e1340fe..6903d3a6087f 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -1264,7 +1264,7 @@ def withNewMutableVars {α} (newVars : Array Var) (mutable : Bool) (x : M α) : def checkReassignable (xs : Array Var) : M Unit := do let throwInvalidReassignment (x : Name) : M Unit := - throwError "`{x.simpMacroScopes}` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `{x.simpMacroScopes}`, consider using `let {x.simpMacroScopes}` instead" + throwError "`{x.simpMacroScopes}` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `{x.simpMacroScopes}`, consider using `let {x.simpMacroScopes}` instead" let ctx ← read for x in xs do unless ctx.mutableVars.contains x.getId do diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out index 2986c334d144..8efb3134cfde 100644 --- a/tests/lean/doNotation1.lean.expected.out +++ b/tests/lean/doNotation1.lean.expected.out @@ -1,6 +1,6 @@ -doNotation1.lean:4:0-4:6: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `y`, consider using `let y` instead -doNotation1.lean:8:2-8:18: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `y`, consider using `let y` instead -doNotation1.lean:12:2-12:17: error: `p` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intent to mutate but define `p`, consider using `let p` instead +doNotation1.lean:4:0-4:6: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `y`, consider using `let y` instead +doNotation1.lean:8:2-8:18: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `y`, consider using `let y` instead +doNotation1.lean:12:2-12:17: error: `p` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `p`, consider using `let p` instead doNotation1.lean:20:7-20:22: error: invalid reassignment, value has type Vector Nat (n + 1) : Type but is expected to have type