Zulip Chat Archive

Stream: general

Topic: notation introduce variables


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Joe Hendrix (Aug 09 2018 at 23:06):

Great. Thanks for finding that.

view this post on Zulip 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