scoped notation in an attribute

Stream: metaprogramming / tactics

[Chris Henson]

In CSLib we have a command and attribute that creates notations. I would like to change these to be scoped the same as the declaration the attribute is applied to. On its own having scoped notation3 in a macro is fine, but will not work from within an attribute. Is there a way I can manually specify the namespace the notation should use?

[Chris Henson]

I had the thought that I could manually assemble the Lean.ParserDescr, but there are several downsides to this:

• for notation3, this doesn't handle the generated delaborators
• even if I add the definition, I'm not sure how that gets registered as notation
• a bit annoying for maintainability

What I feel I need is a way to pass to scoped (within an attribute/macro) what namespace it should be using.

[Eric Wieser]

Does this work?

syntax attrKind "reduction_notation" ident (str)? : command
macro_rules
  | `($kind:attrKind reduction_notation $rs $sym) =>
    `(
      $kind:attrKind notation3 t:39 " ⭢" $sym:str t':39 => (ReductionSystem.Red  $rs) t t'
      $kind:attrKind notation3 t:39 " ↠" $sym:str t':39 => (ReductionSystem.MRed $rs) t t'
     )
  | `($kind:attrKind reduction_notation $rs) =>
    `(
      $kind:attrKind notation3 t:39 " ⭢ " t':39 => (ReductionSystem.Red  $rs) t t'
      $kind:attrKind notation3 t:39 " ↠ " t':39 => (ReductionSystem.MRed $rs) t t'
     )

(found by looking at this line)

[Chris Henson]

Ah, that got me halfway there, thanks! Along with docs#Lean.Elab.Command.modifyScope, I was able to make it work from within an attribute in cslib#133.