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. Mutual Recursion
   2. 4.4.2. Structural Recursion
      1. 4.4.2.1. Explicit Structural Recursion
      2. 4.4.2.2. Mutual Structural Recursion
      3. 4.4.2.3. Inferring Structural Recursion
      4. 4.4.2.4. Elaboration Using Course-of-Values Recursion
   3. 4.4.3. Well-Founded Recursion
   4. 4.4.4. Partial and Unsafe Recursive Definitions
   5. 4.4.5. Controlling Reduction
5. 4.5. Attributes
6. 4.6. Dynamic Typing
7. 4.7. Coercions