specification of Lean syntax

Stream: lean4

[Martin Harrison]

Where is the formal specification of the syntax of the Lean language? I found this conversation and agree that the grammar will not help me to learn Lean. But I want to find out if guided generation of structured output could improve sagredo. Supplying outlines or guidance with "the CFG for Lean4 syntax" would be a first step in this direction - does such a thing exist?

[Jireh Loreaux]

Syntax in Lean is user-extensible, so there is no complete specification.

[Martin Harrison]

Jireh Loreaux said:

Syntax in Lean is user-extensible, so there is no complete specification.

Is there a partial specification of a base syntax? Is there a formal specification of the rules for extensions?

[Shreyas Srinivas]

Lean has a concrete Syntax expressed by the Syntax inductive type

[Shreyas Srinivas]

@loogle Syntax

[Martin Harrison]

thanks

[Shreyas Srinivas]

Here's the link

[Shreyas Srinivas]

The abstract syntax tree is represented by the inductive type Expr

[Martin Harrison]

killer, thanks

[Shreyas Srinivas]

The doc link for Expr

[Shreyas Srinivas]

I am surprised loogle didn't work

[Martin Harrison]

Shreyas Srinivas said:

I am surprised loogle didn't work

was it supposed to respond in this thread or what?

[Shreyas Srinivas]

That's usually how it seems to work

[Shreyas Srinivas]

@Joachim Breitner I checked and loogle is up and running. I think loogle didn't find search results, but I thought the bot normally prints suggestions in the chat. Is this an unimplemented feature for the bot? EDIT: On second thought, is the bot only accessible in some streams or threads?

[Joachim Breitner]

It should have worked.
@loogle Syntax

[loogle]

:exclamation: unknown identifier 'Syntax'
Did you mean "Syntax", Lean.Syntax, or something else?

[Notification Bot]

Martin Harrison has marked this topic as resolved.

[Notification Bot]

Shreyas Srinivas has marked this topic as unresolved.