## Commands - glossary
| Command Name | Purpose / Function | Documentation Link |
| ------------------------------------------------------------------------------------------------------------------------------------------ | --------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| #check | Evaluates and displays the type of an expression. | [Lean 4 Ref: Interacting with Lean](https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/) |
| #eval | Computes and prints the value of an executable expression. | [Lean 4 Ref: Interacting with Lean](https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/) |
| #print | Displays internal information, definition body, or inductive structure of an identifier. | [Lean 4 Ref: Interacting with Lean](https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/) |
| #reduce | Evaluates an expression using kernel beta/delta reduction. | [Lean 4 Ref: Interacting with Lean](https://lean-lang.org/doc/reference/latest/Interacting-with-Lean/) |
| abbrev | Defines a transparent alias (abbreviation) that unfolds eagerly during elaboration. | [Definitions](https://lean-lang.org/doc/reference/latest/Definitions/Definitions/#The-Lean-Language-Reference--Definitions--Definitions) |
| attribute | Adds or removes attributes (such as @[simp], @[inline]) on existing declarations. | [Lean 4 Ref: Attributes](https://lean-lang.org/doc/reference/latest/Attributes/) |
| axiom | Assumes a proposition as true without requiring a proof. | [Axioms](https://lean-lang.org/doc/reference/latest/Axioms/) |
| class | Defines a new type class for ad-hoc polymorphism. | [Type Classes](https://lean-lang.org/doc/reference/latest/Type-Classes/) |
| def | Defines a new constant, function, or term with a specified value. | [Lean 4 Ref: Definitions](https://lean-lang.org/doc/reference/latest/Definitions/) |
| elab | Extends Lean by defining custom syntax elaborators. | [Lean 4 Ref: Elaboration and Compilation](https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/) |
| export | Re-exports identifiers from one namespace into the current scope. | [Lean 4 Ref: Namespaces and Sections](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/) |
| import | Loads modules and exports from another file or library package. | [Source Files and Modules](https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules/) |
| inductive | Defines a new inductive type (algebraic data type or recursive type). | [Inductive Types](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#structures) |
| infix | Defines shorthand binary notation.<br>The `infix` link is to a `LeanNotes page`. | [[infix-command\|LeanNotes infix]], <br>[Lean 4 Ref: Notations and Macros](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/) |
| instance | Defines a type class instance for a specific type. | [Type Classes](https://lean-lang.org/doc/reference/latest/Type-Classes/)[Instance Declarations](https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Declarations/#instance-declarations) |
| lemma | An alias for theorem, typically used for auxiliary results. | [Tactic Reference](https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#tactic-ref-lemmas) |
| macro | Defines custom syntactic macros for term or tactic transformations. | [Lean 4 Ref: Notations and Macros](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/) |
| namespace | Opens a scope that prepends a prefix to all internal identifiers. | [Lean 4 Ref: Namespaces and Sections](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/) |
| notation | Introduces custom mixfix notation or custom mathematical syntax. | [Lean 4 Ref: Notations and Macros](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/) |
| opaque | Declares a definition whose body is hidden from the elaborator during type-checking. | [Definitions](https://lean-lang.org/doc/reference/latest/Definitions/Definitions/#--tech-term-Opaque-constants) |
| open | Opens a namespace so identifiers can be referenced without full qualification. | [Lean 4 Ref: Namespaces and Sections](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/) |
| prefix, postfix | Defines shorthand binary, unary prefix, or unary postfix notation. | [Lean 4 Ref: Notations and Macros](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/) |
| section | Creates a local scope for managing local variables and options. | [Lean 4 Ref: Namespaces and Sections](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/) |
| set_option | Configures compiler settings, pretty-printer options, or linter flags locally. | [Lean 4 Manual: Options](https://lean-lang.org/doc/reference/latest/) |
| structure | Defines a new single-constructor record type with named fields. | [Inductive Types](https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#structures) |
| syntax | Extends Lean's syntax grammar parser. | [Lean 4 Ref: Notations and Macros](https://lean-lang.org/doc/reference/latest/Notations-and-Macros/) |
| theorem | Declares and proves a mathematical proposition (proof is kept opaque for performance). | [Theorems](https://lean-lang.org/doc/reference/latest/Definitions/Theorems/#The-Lean-Language-Reference--Definitions--Theorems) |
| universe | Declares universe levels explicitly for polymorphic definitions. | [Lean 4 Ref: The Type System](https://lean-lang.org/doc/reference/latest/The-Type-System/) |
| variable | Introduces implicit or explicit variables into the local context for subsequent declarations. | [Namespaces and Sections - variables](https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections/#section-variables) |
## Prompt
Lean4:
1. provide a list of all the Lean4 commands in a table as defined below:
2. provide a table in markdown that has 3 columns:
1. the command name
2. the purpose of the command
3. links to more information about the command