infixl with more complicated expression

Stream: general

[Violeta Hernández]

Lean allow me to do this:

local infixl:65 " +ₒ " => (fun x y ↦ x * 2 + y * 3)

However, when writing x +ₒ y, you end up with (fun x y ↦ x * 2 + y * 3) x y instead of the nicer beta-reduced x * 2 + y * 3. Is there some way to sidestep this with a macro?

[Violeta Hernández]

(of course x * 2 + y * 3 is some dummy expression in lieu of what I actually want; I also don't want to declare a new def or abbrev for this expression)

[Kenny Lau]

@Violeta Hernández you can use notation instead

[Kenny Lau]

namespace Foo

notation:100 x:arg "⊹" y:arg => x * 2 + y * 3

theorem bar (a b : Nat) : a ⊹ b = 3 := sorry

end Foo

#check Foo.bar -- Foo.bar (a b : Nat) : a * 2 + b * 3 = 3

[Violeta Hernández]

That's just what I wanted, thank you!

[Kenny Lau]

also you might consider scoped notation instead of local notation

[Violeta Hernández]

Thanks, I think that might be more appropriate for my use case.

[Kyle Miller]

@Kenny Lau Using :arg doesn't match the precedences in Violeta's notation. It doesn't mean arguments to an operator, but arguments to a function application.

The correct analogue would be

notation:65 x:65 "⊹" y:66 => x * 2 + y * 3