What is a command?

Stream: general

[Kevin Buzzard]

Sorry, I'm not a computer scientist, and I'm trying to write a blog post about induction. Is inductive a "command" in Lean 3? I was hoping I would be able to figure this out from the Lean 3 reference manual, which claims in section 2.1 that the built-in commands are listed in section 5 but I can't find the list, unless the list is basically "everything which appears in section 5". I've figured out that #print is a command but right now inductive might be a keyword-like symbol which is not a command as far as I can make out.

[Julian Berman]

I had this exact question recently (though I didn't ask it), but when I couldn't find a formal definition I answered it by cheating and looking at the syntax files for vscode. Not sure that was the greatest idea, but e.g. here for inductive, the vscode extension calls inductive a "definition command", which it seems to want to be a subset of the keywords: https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json#L10

[Julian Berman]

(And then it calls things like #print or #reduce or etc. "commands" without the definition qualifier: https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json#L28-L29 )

[Bryan Gin-ge Chen]

I wouldn't take the names in the syntax highlighting file too seriously; I don't think it follows Lean's "true" grammar particularly closely.

[Sebastian Ullrich]

"definition command" is not a term used in the Lean source (except of course for definition). The Lean 4 parser for them, which is part of the command syntactic category, is called declaration: https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Command.lean#L63-L64.