2 months ago
- Lean uses `:=` for definitions and `=` for comparisons, with type inference for `String`, `Nat`, `Int`.
- `#eval` runs code and displays results in the InfoView, while `#print` can output to terminal.
- Proofs are written with `theorem` and tactics like `unfold`, `decide`, `simp`, and `omega`.
- Function calls use no parentheses or commas: `f a b c`; parentheses are only for grouping expressions.
- `let` bindings allow local definitions inside functions, and the last expression is the return value.
- Functions can be declared in multiple ways, with explicit or implicit types, including anonymous `fun` syntax.
- The universal quantifier `∀` enables proving statements for all possible values of a parameter.
- Implicit arguments `{ }` and instance arguments `[ ]` are automatically filled by Lean, reducing boilerplate.
- Lean is highly interactive: `Command+Click` on any identifier opens its definition or source.