Appendix C: Incomplete chapters (original) (raw)

1. 1. What is Chalk?
2. 1. 1.1. Walkthrough
   2. 1.2. Crates
   3. 1.3. REPL
3. 2. Contribution guide
4. 3. Representing and manipulating types
5. 1. 3.1. The Interner
   2. 3.2. Rust types
   3. 1. 3.2.1. Alias types
         1. 3.2.2. Application types
   4. 3.3. Rust lifetimes
   5. 3.4. Operations
   6. 1. 3.4.1. TypeFoldable and the TypeFolder trait
6. 4. Lowering Rust IR to logic
7. 1. 4.1. Goals and clauses
   2. 4.2. Type equality and unification
   3. 4.3. Implied bounds
   4. 4.4. Lowering rules
   5. 4.5. Opaque types (impl Trait)
   6. 4.6. Well known traits
   7. 4.7. Well-formedness checking
   8. 4.8. Coherence
8. 5. Canonical queries
9. 1. 5.1. Canonicalization
10. 6. Chalk engine
11. 1. 6.1. Major concepts
12. 6.2. Logic
13. 1. 6.2.1. Coinduction
14. 6.3. SLG Solver
15. 7. Chalk recursive solver
16. 1. 7.1. The stack
17. 7.2. Inductive cycles
18. 7.3. The search graph and caching
19. 7.4. Coinduction
20. Appendix A: Glossary and terminology
21. Appendix B: Bibliography
22. Appendix C: Incomplete chapters
23. Appendix D: Publishing Chalk

Incomplete chapters

Some topics yet to be written:

• Elaborate on the proof procedure
• SLG solving – introduce negative reasoning
• Go over how trait impls are selected and checked
• Add a section on higher-ranked trait bounds