unknown constant '_eval.match_1' when calling `whnf`

Stream: lean4

[Tomas Skrivan]

Why am I getting unknown constant '_eval.match_1' when calling whnf on loop with two mutable variables?

import Qq

open Lean Meta Qq in
run_meta
  let e := q(Id.run do
    let mut x : Nat := 0
    let mut y : Nat := 1
    for _ in [0:10] do
      let tmp := y
      y := x + y
      x := tmp
    x)

  let e ← whnf e
  logInfo m!"{e}"

What is happening here? Why is the match statement not defined?

[Jovan Gerbscheid]

The code in the q(...) elaborates to

(have x := 0;
  have y := 1;
  do
  let r ←
    forIn [:10] ⟨x, y⟩ fun x r =>
        have x := r.fst;
        have y := r.snd;
        have tmp := y;
        have y := x + y;
        have x := tmp;
        do
        pure PUnit.unit
        pure (ForInStep.yield ⟨x, y⟩)
  match r with
    | ⟨x, y⟩ => x).run

This includes a match expression, but you cannot create a match expression using q(...). This is because match expressions are elaborated to a constant (in this case _eval.match_1) but this constant isn't put in the environment by q(...).

[Aaron Liu]

Can we make q(...) modify the environment?

[Jovan Gerbscheid]

It's probably not needed to construct match expressions like this in the first place. But yes, I think it should be possible to get that to work.

[Tomas Skrivan]

Thanks! makes sense, at least it would be nice if q(...) would throw an error.