## Stream: lean4

### Topic: How to mactch an operator in Macro_rules

#### Lim, Thing-han (Mar 19 2021 at 06:28):

How can I match an operator in the Macro_rules ?

I am trying to match an operator and do something corresponding to its affix.
For instance,

syntax "{| " term* " |}" : term
macro_rules
| ({| $a$op $b |}) => do match op with | (infixl$[: $prec]?$[(name := $name)]?$[(priority := $prio)]?$op => $f) => sorry | _ => Macro.throwUnsupported  but it doesn't seem to work, and I am not sure what do I miss. #### Sebastian Ullrich (Mar 19 2021 at 08:32): Binary operators do not share a common syntax kind, nor can they be traced back to the original notation command. So whatever you are trying to do, I believe you need a fundamentally different approach. #### Lim, Thing-han (Mar 19 2021 at 09:45): Oh, does it mean that I am not able to identify if a syntax is operator or not, either using macro_rules or via the elaboration monad ? #### Lim, Thing-han (Mar 19 2021 at 09:48): Is is possible to get syntax (or some other structures) after the macro expansion of operators but before type checking ? #### Sebastian Ullrich (Mar 19 2021 at 10:10): Macro expansion and elaboration are intertwined, but you can call expandMacros explicitly to expand as much as possible (including all notations) without elaboration. #### Lim, Thing-han (Mar 19 2021 at 10:36): While using expandMacros to expand the operator notation as much as I want, will I need to first check if the syntax is of some kind of notation ? #### Sebastian Ullrich (Mar 19 2021 at 10:42): I still don't know what you are trying to do #### Lim, Thing-han (Mar 19 2021 at 10:45): I am just trying to write some macros like macro {|$a $op1$b $op2$c ...|}  => (($op2 <$> ($op1 <$> $a <*>$b) <*> \$c) ...)


#### Sebastian Ullrich (Mar 19 2021 at 10:56):

I've never seen idiom brackets that work recursively like this, or are restricted to operators. In any case, the point stands that you cannot really distinguish infix operators from other syntax. But you can unfold them, using expandMacros.

#### Lim, Thing-han (Mar 19 2021 at 10:59):

But that I saw that expandMixfix can match the syntax to see if it's infix, prefix or postfix?

#### Sebastian Ullrich (Mar 19 2021 at 11:00):

You are confusing the definition and the usage of a notation

#### Lim, Thing-han (Mar 19 2021 at 11:02):

Is there documentation or which files should I look into to help me clarify it ?

#### Sebastian Ullrich (Mar 19 2021 at 11:08):

expandMixfix is called when you use the infix` command, not when you use the operator created by it

#### Lim, Thing-han (Mar 19 2021 at 11:09):

Ah ! ok I got it! Thank you!!

Last updated: May 07 2021 at 12:15 UTC