let pattern matching not work

Stream: new members

[AlanHacker]

Hi all! I have a question regarding let bindings and pattern matching.

In "Functional Programming in Lean" 4.3, section exercises, there's an example that uses a inductive type like this:

inductive ToTrace (α : Type) where
| trace : α → ToTrace α

When I try to extract the value inside ToTrace using a let binding like this:

def applyTraced (op : ToTrace (Prim Empty)) (x : Int) (y : Int)
    : WithLog (Prim Empty × Int × Int) Int :=
  let ToTrace.trace p := op
  match p with
  | Prim.plus =>
    save (Prim.plus, x, y) >>= fun () =>
    pure (x + y)
  | Prim.minus =>
    save (Prim.minus, x, y) >>= fun () =>
    pure (x - y)
  | Prim.times =>
    save (Prim.times, x, y) >>= fun () =>
    pure (x * y)

Lean reports an "unknown identifier 'p'" error.

Is there a specific reason why user-defined inductive types (even with a single constructor) are not allowed in let pattern matches?

Thanks in advance!

[Aaron Liu]

Can you provide a #mwe?

[AlanHacker]

inductive Prim (α : Type) : Type where
  | plus  : Prim α
  | minus : Prim α
  | times : Prim α

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

def save {logged : Type} (data : logged) : WithLog logged Unit :=
  { log := [data], val := () }

instance {logged : Type} : Monad (WithLog logged) where
  pure x := { log := [], val := x }
  bind r f :=
    let { log := l₁, val := x } := r
    let { log := l₂, val := y } := f x
    { log := l₁ ++ l₂, val := y }

inductive ToTrace (α : Type) : Type where
  | trace : α → ToTrace α

def applyTraced (op : ToTrace (Prim Empty)) (x y : Int)
    : WithLog (Prim Empty × Int × Int) Int :=
  let ToTrace.trace p := op
  match p with -- unknown identifier 'p'
  | Prim.plus  => save (Prim.plus,  x, y) >>= fun _ => pure (x + y)
  | Prim.minus => save (Prim.minus, x, y) >>= fun _ => pure (x - y)
  | Prim.times => save (Prim.times, x, y) >>= fun _ => pure (x * y)

I was expecting the pattern let ToTrace.trace p := op to work, since ToTrace only has one constructor.

[Aaron Liu]

def applyTraced (op : ToTrace (Prim Empty)) (x y : Int)
    : WithLog (Prim Empty × Int × Int) Int :=
  let .trace p := op
  match p with
  | Prim.plus  => save (Prim.plus,  x, y) >>= fun _ => pure (x + y)
  | Prim.minus => save (Prim.minus, x, y) >>= fun _ => pure (x - y)
  | Prim.times => save (Prim.times, x, y) >>= fun _ => pure (x * y)

[AlanHacker]

Thanks! That works — but I’m curious, why does this work?

[Aaron Liu]

I don't know, it must be something with the parsing

[Kyle Miller]

This is another workaround:

let (ToTrace.trace p) := op

Without the parentheses, it's interpreting the let as defining a new local function named ToTrace.trace.