5. Source Files

1. 5.1. Files
   1. 5.1.1. Modules
      1. 5.1.1.1. Encoding and Representation
      2. 5.1.1.2. Concrete Syntax
         1. 5.1.1.2.1. Whitespace
         2. 5.1.1.2.2. Comments
         3. 5.1.1.2.3. Keywords and Identifiers
      3. 5.1.1.3. Structure
         1. 5.1.1.3.1. Module Headers
         2. 5.1.1.3.2. Commands
      4. 5.1.1.4. Contents
   2. 5.1.2. Packages, Libraries, and Targets
2. 5.2. Module Contents
   1. 5.2.1. Commands and Declarations
      1. 5.2.1.1. Definition-Like Commands
      2. 5.2.1.2. Modifiers
      3. 5.2.1.3. Signatures
      4. 5.2.1.4. Headers
   2. 5.2.2. Namespaces
   3. 5.2.3. Section Scopes
      1. 5.2.3.1. Controlling Section Scopes
      2. 5.2.3.2. Section Variables
      3. 5.2.3.3. Scoped Attributes
3. 5.3. Axioms
4. 5.4. Attributes
5. 5.5. Dynamic Typing
6. 5.6. Coercions
   1. 5.6.1. Coercion Insertion
   2. 5.6.2. Coercing Between Types
      1. 5.6.2.1. Implementing Coercions
      2. 5.6.2.2. Coercions from Natural Numbers and Integers
   3. 5.6.3. Coercing to Sorts
   4. 5.6.4. Coercing to Function Types
   5. 5.6.5. Implementation Details
      1. 5.6.5.1. Unfolding Coercions
      2. 5.6.5.2. Coercion Chaining