## Stream: general

### Topic: notation introduce variables

#### Joe Hendrix (Aug 09 2018 at 22:24):

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 (Aug 09 2018 at 22:30):

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 (Aug 09 2018 at 22:32):

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

#### Simon Hudon (Aug 09 2018 at 22:42):

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 (Aug 09 2018 at 23:06):

Great. Thanks for finding that.

#### Simon Hudon (Aug 09 2018 at 23:10):

:+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

Last updated: May 11 2021 at 23:11 UTC