1. The Idris 2 Programming Langauge
3. Core Language Features
4. 1. Introduction
5. 1. 1.1. About The Idris Programming Language
   2. 1.2. Using the REPL
   3. 1.3. A First Idris Program
   4. 1.4. The Shape of an Idris Definition
   5. 1.5. Where to Get Help
   6. 1.6. Conclusion
6. 2. Introduction To Functions
7. 1. 2.1. Functions With More Than One Argument
   2. 2.2. Function Composition
   3. 2.3. Higher Order Functions
   4. 2.4. Currying
   5. 2.5. Anonymous Functions
   6. 2.6. Operators
   7. 2.7. Introductory Function Exercises
   8. 2.8. Conclusion
8. 3. Algebraic Data Types
9. 1. 3.1. Enumerations
   2. 3.2. Exercises
   3. 3.3. Sum Types
   4. 3.4. Exercises
   5. 3.5. Records
   6. 3.6. Exercises
   7. 3.7. Generic Data Types
   8. 3.8. Exercises
   9. 3.9. Alternative Syntax for Data Definitions
   10. 3.10. Conclusion
10. 4. Interfaces
11. 1. 4.1. Interface Basics
    2. 4.2. Exercises
    3. 4.3. More About Interfaces
    4. 4.4. Exercises
    5. 4.5. Interfaces in the Prelude
    6. 4.6. Exercises
    7. 4.7. Conclusion
12. 5. Functions Part 2
13. 1. 5.1. Let Bindings and Local Definitions
    2. 5.2. Exercises
    3. 5.3. The Truth about Function Arguments
    4. 5.4. Programming with Holes
    5. 5.5. Conclusion
14. 6. Dependent Types
15. 1. 6.1. Length-Indexed Lists
    2. 6.2. Exercises
    3. 6.3. Fin: Safe Indexing Into Vectors
    4. 6.4. Exercises
    5. 6.5. Compile-Time Computations
    6. 6.6. Exercises
    7. 6.7. Conclusion
16. 7. IO: Programming with Side Effects
17. 1. 7.1. Pure Side Effects?
    2. 7.2. Exercises
    3. 7.3. Do Blocks, Desugared
    4. 7.4. Exercises
    5. 7.5. Working With Files
    6. 7.6. Exercises
    7. 7.7. How IO is Implemented
    8. 7.8. Conclusion
18. 8. Functor and Friends
19. 1. 8.1. Functor
    2. 8.2. Exercises
    3. 8.3. Applicative
    4. 8.4. Exercises
    5. 8.5. Monad
    6. 8.6. Exercises
    7. 8.7. Background and further Reading
    8. 8.8. Conclusion
20. 9. Recursion and Folds
21. 1. 9.1. Recursion
    2. 9.2. Exercises
    3. 9.3. Notes on Totality Checking
    4. 9.4. Exercises
    5. 9.5. Interface Foldable
    6. 9.6. Exercises
    7. 9.7. Conclusion
22. 10. Effectful Traversals
23. 1. 10.1. Reading CSV Tables
    2. 10.2. Exercises
    3. 10.3. Programming with State
    4. 10.4. Exercises
    5. 10.5. The Power of Composition
    6. 10.6. Exercises
    7. 10.7. Conclusion
24. 11. Sigma Types
25. 1. 11.1. Dependent Pairs
    2. 11.2. Exercises
    3. 11.3. Use Case: Nucleic Acids
    4. 11.4. Exercises
    5. 11.5. Use Case: CSV Files with a Schema
    6. 11.6. Exercises
    7. 11.7. Conclusion
26. 12. Propositional Equality
27. 1. 12.1. Equality as a Type
    2. 12.2. Exercises
    3. 12.3. Programs as Proofs
    4. 12.4. Exercises
    5. 12.5. Into the Void
    6. 12.6. Exercises
    7. 12.7. Rewrite Rules
    8. 12.8. Exercises
    9. 12.9. Conclusion
28. 13. Predicates and Proof Search
29. 1. 13.1. Preconditions
    2. 13.2. Exercises
    3. 13.3. Contracts between Values
    4. 13.4. Exercises
    5. 13.5. Use Case: Flexible Error Handling
    6. 13.6. Exercises
    7. 13.7. The Truth about Interfaces
    8. 13.8. Conclusion
30. 14. Primitives
31. 1. 14.1. How Primitives are Implemented
    2. 14.2. Working with Strings
    3. 14.3. Exercises
    4. 14.4. Integers
    5. 14.5. Exercises
    6. 14.6. Refined Primitives
    7. 14.7. Exercises
35. Appendices
36. 15. Getting Started with pack and Idris 2
37. 16. Interactive Editing in Neovim
38. 17. Structuring Idris Projects
39. 18. A Deep Dive into Quantitative Type Theory
43. Exercise Solutions
44. 19. Introductory Function Exercises
45. 20. Algebraic Data Types
46. 21. Interfaces
47. 22. Functions Part 2
48. 23. Dependent Types
49. 24. IO: Programming with Side Effects
50. 25. Functor and Friends
51. 26. Recursion and Folds
52. 27. Effectful Traversals
53. 28. Sigma Types
54. 29. Propositional Equality
55. 30. Predicates and Proof Search
56. 31. Primitives