Skip to content

Commit

Permalink
fix: correct typo in invalid reassignment error (leanprover#5080)
Browse files Browse the repository at this point in the history
Corrects a small typo in the error message for when a user attempts to
mutate something which cannot be mutated.
  • Loading branch information
mtoohey31 authored Aug 18, 2024
1 parent 38288ae commit b486c67
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion src/Lean/Elab/Do.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions tests/lean/doNotation1.lean.expected.out
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit b486c67

Please sign in to comment.