quote4
quote4 copied to clipboard
`let mut` does not work with `~q` matching
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 usinglet mut
can be mutated. If you did not intent to mutate but definex
, consider usinglet 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