• Intro: introduction to Equations, demonstrating its features (source).

Dependent Pattern-Matching

Recursion