Where is the Lean syntax documented?

Stream: new members

[Dan Abramov]

I know it might sound like I'm trolling but I swear I'm not. I wanted to look up the def ... where syntax. In particular, I want to understand what you're supposed to put into where and what this style desugars to (if anything).

I googled "lean def where syntax". One of the first hits is someone asking where Lean syntax is supposed to be documented — I'm glad I'm not alone. A recent answer suggests the place to look for is the "reference manual".

I go to the reference manual and type where in search. There is a hit!

Screenshot 2025-09-08 at 19.32.18.png

I press that, and land on this section:

Screenshot 2025-09-08 at 19.32.40.png

However, all I can find about where is this one sentence with grammar:

Screenshot 2025-09-08 at 19.34.53.png

Is this implied to be sufficient documentation on where for a language reference? Or is this page generally considered unfinished, and more work is planned to flesh it out? In the meantime, is there a location where I can learn what the syntax of where is, and what it desugars to (if anything)?

[Dan Abramov]

I'm guessing that

def foo : T where
  field1 := value1
  field2 := value2

is syntax sugar for

def foo : T := {
  field1 := value1
  field2 := value2
}

Is that correct? If yes, would it be reasonable to add that to the docs?

[Dan Abramov]

The concrete reason for how I ran into this is that I tried to use this where syntax inline (inside a let) and it didn't work, and I didn't know what it does so I got stuck.

[Kyle Miller]

It seems your main question here is asking for confirmation about the syntax sugar: yes, correct, where ... is := { ... }. Not to be confused for the where in def f a b c := v where ..., which instead is def f a b c := let rec ...; v.

Is this implied to be sufficient documentation on where for a language reference? Or is this page generally considered unfinished, and more work is planned to flesh it out?

I don't believe you'll find answers to these questions here in #new members. David Christiansen has been writing the language reference, and I think he doesn't frequent this channel. (Feel free to ping him.)

If you need to know exactly what features are available, probably the most accurate way to find the available syntaxes is to search for "where and " where in the Lean source code; that will bring you to Lean.Parser.Command.whereStructInst, and then you can click around to work out the grammar. Anticipating your followup to that: yeah, that's not the intended way to learn Lean, but if you need the exact answers it's nice to know that it's available.

There's also the Zulip search box. This is a significant part of the current Lean documentation. I relied on it heavily when learning Lean 3.

I understand where come from with your questions, thinking about it from high-level product design and the experience of newcomers, but at least for me it'd be helpful if you'd separate focused technical questions from broader "here's my user experience, is this how it's intended to go?" discussion; unblocking you right now vs the meta question of how to not be blocked. The latter is broad and open-ended — and valuable — but it might be more effective in a separate topic, in GitHub issues, in write-ups of your experiences, etc. Or if writing out your experience helps you learn and you're ok with getting whatever engagement you get, that's fine too.

[Dan Abramov]

Thanks! I'm sorry for mixing up rants and questions. I don't have the energy to channel rants into something more productive yet (like PRs) and I'm not sure where to direct them "appropriately". I think partially I'm just trying to get a temperature check on whether it's "yes, this kinda sucks" or more like "no, we think this is how it should be".

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

If you need to know exactly what features are available, probably the most accurate way to find the available syntaxes is to search for "where and " where in the Lean source code

To add to this, if you import Lean at the top of the file, 'Go to declaration' (not 'Go to definition') in VsCode will usually take you to the relevant syntax definition.

[Kyle Miller]

Somehow where goes to structInst term syntax, not where @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒. Maybe some macro expansion information is missing from the info trees?