The Lean Language Reference
The Lean Language Reference
Table of Contents
1.
Introduction
2.
Elaboration and Compilation
3.
Interacting with Lean
4.
The Type System
5.
Source Files and Modules
6.
Namespaces and Sections
7.
Definitions
8.
Axioms
9.
Attributes
10.
Terms
11.
Type Classes
12.
Coercions
13.
Tactic Proofs
14.
Functors, Monads and
do
-Notation
15.
IO
16.
The Simplifier
17.
The
grind
tactic
18.
Basic Propositions
19.
Basic Types
20.
Dynamic Typing
21.
Standard Library
22.
Notations and Macros
23.
Run-Time Code
24.
Build Tools and Distribution
Release Notes
Index
Progress
17.
The
grind
tactic
17.1.
Quick Start
17.2.
What is
grind
?
17.3.
What
grind
is
not
.
17.4.
Congruence Closure
17.5.
Debugging tip
17.6.
Constraint Propagation
17.7.
Case Analysis
17.8.
E‑matching
17.9.
Linear Integer Arithmetic Solver
17.10.
Algebraic Solver (Commutative Rings, Fields)
17.11.
Normalizer / Pre‑processor
17.12.
Diagnostics
17.13.
Troubleshooting & FAQ
17.14.
Bigger Examples
17.11.
Normalizer / Pre‑processor
Source Code
Report Issues
←
17.10. Algebraic Solver (Commutative Rings, Fields)
17.12. Diagnostics
→
17.11. Normalizer / Pre‑processor
TBD Canonicalization pass; extending with
[grind norm]
(expert only).
←
17.10. Algebraic Solver (Commutative Rings, Fields)
17.12. Diagnostics
→
