pattern match for `Prod`

Stream: general

[Asei Inoue]

How to resolve this error?

import Lean

inductive BinTree (α : Type) where
  | empty
  | node (val : α) (left right : BinTree α)
deriving DecidableEq, BEq

variable {α : Type}
variable {m : Type → Type} [Monad m]

open Std

def BinTree.bfs (t : BinTree α) (action : α → m Unit) : m Unit := do
  let mut queue : Queue (BinTree α) := ⟨[t], []⟩
  while ! queue.isEmpty do
    match queue.dequeue? with
    | none => break
    /- unsupported pattern in syntax match
       some (node, q') -/
    | some (node, q') =>
      queue := q'
      match node with
      | .empty => continue
      | .node v left right => do
        action v
        queue := queue.enqueue left
        queue := queue.enqueue right

[Aaron Liu]

Probably node is being treated as BinTree.node does using some other name work