matching on syntax alternatives

Stream: metaprogramming / tactics

[Edward van de Meent]

i'd like to match on a syntax rule wich contains l <|> r with syntax quotations.
Is there a way to do this which introduces variables l : Option (TSyntax ``l) and r : Option (TSyntax ``r)? or maybe somehow get Sum (TSyntax ``l) (TSyntax ``r)?

(my concrete usecase is that I'd like to extract the head ident from docs#Lean.Parser.Tactic.inductionAltLHS with only two match branches, where the second returns throwUnsupportedSyntax)

[Aaron Liu]

I think l <|> r is an "untagged" sum, so you need to differentiate it by hand.

[Edward van de Meent]

how do you mean "untagged"? do you mean that there is no syntax node where we can see that indeed this part of syntax matches an alternative?

[Aaron Liu]

For example, docs#Sum is tagged, since the extra constructor on top means you can distinguish .inl () from .inr (), but the representation of l <|> r doesn't have that extra layer.

[Aaron Liu]

Oh, misread the symbol. Disregard everything I just said.