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. Matching Pairs vs Simultaneous Matching
      2. 4.4.1.2. Mutual Structural 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