Index.md

A Tutorial on Elaborator Reflection in Idris 2

Idris 2 elaborator reflection provides programmers with a powerful and clean toolkit for writing metaprograms.

This is a tutorial consisting of several loosely related posts / articles about different aspects and techniques available in elaborator reflection. It was written - and is still being extended - in the hope that others might find it useful. Have fun.

Table of Contents

1. A short Introduction to Metaprogramming
2. Inspecting the Structure of Idris Expressions
3. Automatic Generation of Enumerations
   1. A First Metaprogram: Defining Enumerations
   2. Interface Implementations for Enumerations
4. Generics
   1. Sums of Products: A Generic Representation for Algebraic Data Types
   2. The Challenges of Parameterized Data Types
   3. Deriving Generic for Parameterized Data Types
   4. Generic Deriving of Interface Implementations
   5. Type checked Elaborator Scripts
   6. Verified Interfaces Part 1
   7. Verified Interfaces Part 2
5. Refined Primitives
6. Deriving Functionality for Data Types