on-click have? using h

Stream: mathlib4

[Floris van Doorn]

When clicking on a suggestion produced by have? using h, the word have? is replaced by the suggestion, but the using h remains at the end of the line.

[Floris van Doorn]

I think I can fix this myself. One question:
If I have a snippet

elab_rules : tactic
  | `(tactic| have?%$tk using $term) => do ...

In the do I want to refer to the whole syntax object have? using ... How do I do this? Is ← getRef the usual way to do this? Is there also a way to give that syntax a name in the pattern match?

[Floris van Doorn]

!4#5305

[Kyle Miller]

I don't know if you can give a name to the whole syntax object from within the pattern, but my understanding is that getRef will give you the Syntax (at least both evalTactic and elabCommand have a withRef to set it to the right thing).

[Mario Carneiro]

You should be able to get a reference to the syntax via | stx@`(tactic| have? ...) => ...

[Kyle Miller]

I agree you should be able to, but you get an "unexpected syntax" error

[Kyle Miller]

I'm not remembering where in the source code it is, but match expressions with quotations for cases is its own whole elaborator, and it appears not to support @ based on this

[Mario Carneiro]

you can also break open elab_rules a bit and write a @[tactic] def directly

[Kyle Miller]

(here's the match elaborator for quotations)

[Kyle Miller]

Hmm, match accepts it but elab_rules doesn't. I guess this means it's actually the part of elab_rules that tries to figure out which attributes to set that's failing when there's an @?

[Kyle Miller]

The exception seems to be this line, were it gives up if the match pattern isn't immediately syntax quotation: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/ElabRules.lean#LL28C9-L28C31