• Monads
• General monadology
• Important metaprogramming monads
• Objects
• Syntax
• LocalDecl
• LocalContext
• Names
• Expressions
• Metavariables
• Free variables
• Bound variables
• Lambdas
• Foralls
• Applications
• The rest
• MVarId
• FVarId
• Goals
• Tactics
• Macros
• Antiquotations
• Debugging / Logging