Inaccessible names in tactic state

Stream: metaprogramming / tactics

[Eric Wieser]

The tactic state at the comment in this code:

meta def what : tactic unit :=
do
  (a, 1) ← pure (⟨2, 3⟩ : ℕ × ℕ) | do {
    -- if I put my cursor at the start of this line, I can see `_x` and `_p`.
    -- why can't I refer to these except with `‹›`? Which one is being found?
    tactic.trace format!"where did this come from: {‹ℕ × ℕ›}"
  },
  tactic.skip

run_cmd what

is

what: tactic unit
_p: ℕ × ℕ
_do_match: ℕ × ℕ → tactic unit
_x: ℕ × ℕ
⊢ ℕ × ℕ

What are _x and _p, and is there any way for me to access them?

[Jannis Limperg]

These are artifacts of the equation compiler like the _do_match. I'm surprised you can even access them with the French quotes. You definitely shouldn't use them; conceptually there are no variables _x and _p in scope at that program point (or anywhere).

[Eric Wieser]

Well, conceptually there is an "object for which the match failed" which is not otherwise accessible with that | syntax

[Eric Wieser]

Looking at the output of #print, it looks like _x and _p are one and the same

[Jannis Limperg]

Right. If you need the matched object, I guess your least inelegant bet is

x <- ...,
(y, z) <- pure x | fail! "Matched object: {x}",

Or of course a good old match.