Macro expanding to binder

Stream: lean4

[Adam Topaz]

I'm trying to figure out whether it's possible to write a macro that expands to a binder.
As a simple example, let's say I want [[foo X]] to expand to [Mul X] [Add X] and to be able to write things like

def test (X : Type) [[foo X]] (x : X) : X := x + x * x

Is this possible?

[Mario Carneiro]

no

[Mario Carneiro]

not unless you replace def

[Mario Carneiro]

or change core, of course

[Adam Topaz]

Okay, thanks. That's unfortunate.

[Adam Topaz]

Semirelated: does lean4/mathlib4 have an analogue of docs#lean.parser.emit_code_here

[James Gallicchio]

Mario Carneiro said:

not unless you replace def

(replace = overload?)

[Mario Carneiro]

Adam Topaz said:

Semirelated: does lean4/mathlib4 have an analogue of docs#lean.parser.emit_code_here

It's not really necessary, as you can just call elabCommand with whatever syntax you like

[Mario Carneiro]

James Gallicchio said:

Mario Carneiro said:

not unless you replace def

(replace = overload?)

No, overload here would presumably mean defining a new elab_rules for the existing syntax, while in this case you would want to create a new syntax that shadows the old one

[Mario Carneiro]

they have a similar effect, but one changes the behavior while the other changes the syntax

[Tomas Skrivan]

Recently I had the same question, there is a code example for overloading lambda function notation.