Typed Macro Issues?

Stream: lean4

[François G. Dorais]

I'm running into a couple of issues updating code after the "Typed Macro" update. I managed to fix them all so far but I'm puzzled by some of the solutions.

For example, this macro:

macro "mwe" name:ident rest:tacticSeq : tactic => `(tactic| intro $name:ident; ($rest))

Doesn't work without specifying $name:ident on the RHS. It seems like intro expects a matchAlt argument by default instead of an ident. This is probably a bug.

The parentheses around $rest are also necessary for some reason. This might be a feature but I don't understand why this is necessary.

[Sebastian Ullrich]

Thanks for the feedback! The intro issue is an artifact resulting from the fact that there are actually two separate intro tactics, for idents and for matchAlts, would be feasible but maybe a bit complex to make that still work. The second issue is "technically correct", without parentheses Lean expects a single tactic at that point. We could define a coercion to insert the parentheses for us.

[François G. Dorais]

Thanks Sebastian! That makes sense. The $rest issue makes total sense now. It would be convenient to have a coercion since I had quite a few cases of that to fix.

Thanks for the explanation of the intro issue! Is this an instance "the matchAlt case is tried before the ident case because the matchAlt case was defined last" or is it more complex than that?

[Sebastian Ullrich]

intro $name is in fact parsed into a choice node of both tactics

     [(choice
       (Tactic.intro "intro" [(term.pseudo.antiquot "$" [] `name [])])
       (Tactic.introMatch "intro" (Term.matchAlts.antiquot "$" [] `name [])))

We would have to select and generate the correct alternative given name : TSyntax [`term, `matchAlt]