# Zulip Chat Archive

## 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