4. Source Files

1. 4.1. Files
   1. 4.1.1. Modules
      1. 4.1.1.1. Encoding and Representation
      2. 4.1.1.2. Concrete Syntax
         1. 4.1.1.2.1. Whitespace
         2. 4.1.1.2.2. Comments
         3. 4.1.1.2.3. Keywords and Identifiers
      3. 4.1.1.3. Structure
         1. 4.1.1.3.1. Module Headers
         2. 4.1.1.3.2. Commands
      4. 4.1.1.4. Contents
   2. 4.1.2. Packages, Libraries, and Targets
2. 4.2. Module Contents
   1. 4.2.1. Commands and Declarations
      1. 4.2.1.1. Definition-Like Commands
      2. 4.2.1.2. Modifiers
      3. 4.2.1.3. Signatures
      4. 4.2.1.4. Headers
   2. 4.2.2. Namespaces
   3. 4.2.3. Section Scopes
      1. 4.2.3.1. Controlling Section Scopes
      2. 4.2.3.2. Section Variables
      3. 4.2.3.3. Scoped Attributes
3. 4.3. Axioms
4. 4.4. Recursive Definitions
   1. 4.4.1. Structural Recursion
      1. 4.4.1.1. Explicit structural recursion
      2. 4.4.1.2. Mutual structural recursion
      3. 4.4.1.3. Inferring structural recursion
      4. 4.4.1.4. Elaboration using course-of-value recursion
   2. 4.4.2. Well-Founded Recursion
   3. 4.4.3. Controlling Reduction
   4. 4.4.4. Partial and Unsafe Recursive Definitions
5. 4.5. Attributes
6. 4.6. Dynamic Typing
7. 4.7. Coercions