conv and case

Stream: lean4

[Simon Hudon]

Is there an equivalent to case tag => inside the conv tactic language?

[Mario Carneiro]

I would guess it should be case tag =>

[Mario Carneiro]

it probably doesn't exist but you can make one yourself

[Mario Carneiro]

although I don't know how to make tags in a conv block in the first place

[Simon Hudon]

I'm looking at the elaborators for conv tactics and they seem to just exist inside the TacticM monad. case should have a very similar implementation inside conv and inside tactic

[Simon Hudon]

Update: copy pasting the case elaborator works for conv (with a few replacements like evalTactic -> evalConvSeq and tacticSeq -> convSeq)