name for syntax category of `notation`, `namespace`, `def`..

Stream: lean4

[Asei Inoue]

I have seen top-level commands starting with #, such as #check and #reduce, referred to as "diagnostic commands". On the other hand, are there any customary terms for other commands such as def or notation?

[Asei Inoue]

The commands group I have a question about here are as follows:

• def
• noncomputable
• notation
• infix
• prefix
• postfix
• open
• namespace
• class
• inductive
• structure
• ....

[Asei Inoue]

The question is: "Is there a short word for a top-level command that does not start with #?

[Eric Wieser]

Syntactically, there is nothing special about #print vs def; both are in the command category

[Asei Inoue]

Syntactically, there is nothing special about #print vs def; both are in the command category

That's why I'm in trouble ...

[Asei Inoue]

I want a customary name for it, rather than a syntactic classification name.

[Asei Inoue]

Would it be strange if I called it "syntactic command"?

[Damiano Testa]

Maybe def, theorem,... can be called "keywords"?

The linter that excludes #-commands is called... docs#Mathlib.Linter.linter.hashCommand, but this is not an official name.

[Asei Inoue]

"keyword" sounds nice. It can be called "syntactic keyword"?

[Max Nowak 🐉]

I’d call them declarations

[Max Nowak 🐉]

Except namespace, section, etc

[Eric Wieser]

Asei, can you elaborate on why you want a name for these?

[Eric Wieser]

Max Nowak 🐉 said:

I’d call them declarations

Declarations are the things (some of) these keywords generate, not the keywords themselves

[Max Nowak 🐉]

Internally, def, inductive, etc elaborate the syntax tree, and then use the “addDecl” function to add the actual declaration to the Environment.

[Eric Wieser]

So maybe "declaration commands" would be reasonable, but I don't think this ends up being referred to often enough to need a name

[Eric Wieser]

And example doesn't create a declaration at all!

[Asei Inoue]

Asei, can you elaborate on why you want a name for these?

Commands with # and without # seem to have different uses and appearances, but I thought it was inconvenient not to have a concise name for them.

[Eric Wieser]

I guess #align and #align_import are exceptions to that rule

[Asei Inoue]

oh its really an exception...

[Damiano Testa]

The expectation is that all such exceptions are in

private abbrev allowed_commands : HashSet String :=
  { "#align", "#align_import", "#noalign", "#adaptation_note" }

[Mac Malone]

Eric Wieser said:

And example doesn't create a declaration at all!

Nonetheless, it is part of the declaration syntax. :laughing: :wink:

[Mac Malone]

(It actually does create a declaration. It just then discards it via withoutModifyingEnv).