Skip to content

Commit b486c67

Browse files
authored
fix: correct typo in invalid reassignment error (#5080)
Corrects a small typo in the error message for when a user attempts to mutate something which cannot be mutated.
1 parent 38288ae commit b486c67

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

src/Lean/Elab/Do.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1264,7 +1264,7 @@ def withNewMutableVars {α} (newVars : Array Var) (mutable : Bool) (x : M α) :
12641264

12651265
def checkReassignable (xs : Array Var) : M Unit := do
12661266
let throwInvalidReassignment (x : Name) : M Unit :=
1267-
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"
1267+
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"
12681268
let ctx ← read
12691269
for x in xs do
12701270
unless ctx.mutableVars.contains x.getId do

tests/lean/doNotation1.lean.expected.out

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
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
2-
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
3-
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
1+
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
2+
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
3+
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
44
doNotation1.lean:20:7-20:22: error: invalid reassignment, value has type
55
Vector Nat (n + 1) : Type
66
but is expected to have type

0 commit comments

Comments
 (0)