notation introduce variables

Stream: general

[Joe Hendrix]

Is it possible to write notation that will allow introducing variables? e.g. have something like the following work:

local notation `flet` var `:=` rhs `fin` body := let var := rhs in body
example : ℕ := flet x := 1 fin x

[Simon Hudon]

Yes, the following can be found in core.lean: notation `exists` binders `, ` r:(scoped P, Exists P) := r which illustrates how the binder / scoped notation works.

It let's you tell Lean how to parse a lambda abstract and choose a function (i.e. Exists) to feed that lambda expression to.

[Simon Hudon]

I think your notation could work as local notation `flet` binder `:=` rhs `fin` body:(scoped P, P rhs) := body

[Simon Hudon]

To help with the pretty printing, you may way to define a function that Lean will associate with your notation:

def my_let {α β : Sort*} (f : α → β) (x : α) := f x

local notation `flet` binder `:=` rhs `fin` body:(scoped P, my_let P rhs) := body

[Joe Hendrix]

Great. Thanks for finding that.

[Simon Hudon]

:+1: To be fair, a few months back, there was intense session on gitter, looking through the C++ code and figuring out the ins and outs of the notation notation