apply? using tombstones

Stream: lean4

[Michael Stoll]

I noticed recently (but can't tell exactly when) that the suggestions apply? produces frequently contain names with tombstone; e.g.

example (a b : Nat) : a - b = 0 := by
  -- First suggestion is "Try this: refine Eq.symm (Nat.eq_of_beq_eq_true ?a✝)"
  apply?

(There are more suggestions, and not all of them have tombstones.)

This is annoying, as clicking on the suggestion gives you an error, and you have to remove the ✝ to make it work.

[Joachim Breitner]

It’s a known issue, but there isn’t really a good way to fix that. I guess understanding how to make inaccessible parameters accessible is something that for now we have to expert the user to do.

[Kyle Miller]

It could set pp.mvars to false before pretty printing. I don't expect mvar names to be useful in the apply? output.

[Joachim Breitner]

Oh, it's an mvar, not a daggered hypothesis here. Sorry for not reading carefully

[Kim Morrison]

lean#6108