Topic: What is a command?
Kevin Buzzard (Apr 03 2021 at 15:17):
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
inductive might be a keyword-like symbol which is not a command as far as I can make out.
Julian Berman (Apr 03 2021 at 15:21):
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 (Apr 03 2021 at 15:22):
(And then it calls things like
#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 (Apr 03 2021 at 15:29):
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 (Apr 03 2021 at 15:40):
"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
Last updated: May 15 2021 at 00:39 UTC