refactoring mathport syntax?

Stream: mathlib4

[Thomas Murrills]

In tfae_have (!4#2062), I refactor the syntax

syntax (name := tfaeHave) "tfae_have " (ident " : ")? num (" → " <|> " ↔ " <|> " ← ") num : tactic

to

syntax impArrow := " → " <|> " ↔ " <|> " ← "
syntax (name := tfaeHave) "tfae_have " (ident " : ")? num impArrow num : tactic

so that I can easily parse the arrows.

Is this allowed in mathport, or does changing the name of the component syntax node mess things up?

[Gabriel Ebner]

Please don't worry too much about changing the syntax, but it will require changes in mathport because right now it's constructing the syntax tree manually. So please ping me or Mario when the change lands.

[Thomas Murrills]

@Gabriel Ebner or @Mario Carneiro , tfae_have has just landed, so here's the requested ping :)

[Gabriel Ebner]

Looks like the auto-update went without a hitch: https://github.com/leanprover-community/mathport/actions/workflows/update.yml

[Mario Carneiro]

actually the new version of the syntax can be written more compactly now rather than splitting into cases for each direction of the arrow, although the old code will still work

[Thomas Murrills]

do you mean something like writing syntax " → " : impArrow (plus the rest) instead or am I (likely) misunderstanding?

[Mario Carneiro]

I mean the mathport code can be improved