←
Prev
↑
Up
Next
→
The Lean Language Reference
1.
Introduction
2.
Elaboration and Compilation
3.
The Type System
4.
Source Files
5.
Recursive Definitions
6.
Terms
7.
Type Classes
8.
Functors, Monads and
do
-Notation
9.
IO
10.
Tactic Proofs
11.
The Simplifier
12.
Basic Types
13.
Standard Library
14.
Notations and Macros
15.
Output from Lean
16.
Elan
17.
Lake and Reservoir
Index
4.
Source Files
4.1.
Files
4.2.
Module Contents
4.3.
Axioms
4.4.
Attributes
4.5.
Dynamic Typing
4.6.
Coercions
Source Code
Report Issues
4. Source Files
4.1.
Files
4.1.1.
Modules
4.1.1.1.
Encoding and Representation
4.1.1.2.
Concrete Syntax
4.1.1.2.1.
Whitespace
4.1.1.2.2.
Comments
4.1.1.2.3.
Keywords and Identifiers
4.1.1.3.
Structure
4.1.1.3.1.
Module Headers
4.1.1.3.2.
Commands
4.1.1.4.
Contents
4.1.2.
Packages, Libraries, and Targets
4.2.
Module Contents
4.2.1.
Commands and Declarations
4.2.1.1.
Definition-Like Commands
4.2.1.2.
Modifiers
4.2.1.3.
Signatures
4.2.1.4.
Headers
4.2.2.
Namespaces
4.2.3.
Section Scopes
4.2.3.1.
Controlling Section Scopes
4.2.3.2.
Section Variables
4.2.3.3.
Scoped Attributes
4.3.
Axioms
4.4.
Attributes
4.5.
Dynamic Typing
4.6.
Coercions