quote4 icon indicating copy to clipboard operation
quote4 copied to clipboard

`let mut` does not work with `~q` matching

Open eric-wieser opened this issue 4 months ago • 0 comments

This complains on each x :=

import Qq
open Qq Lean

example : MetaM Nat := do
  let mut x := 1
  if let ~q(Prop) := q(Type) then
    x := 2
  else
    x := 3
  return x

with error

x cannot be mutated, only variables declared using let mut can be mutated. If you did not intent to mutate but define x, consider using let x instead

Normally this would be legal:

example : MetaM Nat := do
  let mut x := 1
  if let true := false then
    x := 2
  else
    x := 3
  return x

This is almost certainly related to #21

eric-wieser avatar Feb 18 '24 11:02 eric-wieser