Gallery of programs Intro: introduction to Equations, demonstrating its features (source). Dependent Pattern-Matching Polynomials: a reflexive tactic for solving boolean tautologies (source). HoTT_light: basics of the HoTT library implemented using a logic in Type (source). MoreDep: part of chapter 8 of Adam Chlipala’s CPDT (source). Definitional interpreter: definitional interpreter for an impure language using well-scoped, well-typed syntax (source). Views: using dependent pattern-matching with views, to handle default cases in pattern-matching (source). Recursion STLC: strong normalization of simply-typed lambda-calculus with products using hereditary substitutions (source). String Matching: beginning of example by Nicky Vazou on string matching, uses well-founded recursion (source). Rose Trees: nested well-founded recursion (source). Nested mutual recursion: structural mutual and nested recursion (source). Accumulators: defining and proving programs using accumulators, with well-founded recursion (source). Mutual well-founded recursion: representing mutually recursive well-founded definitions using dependent pattern-matching (source). General recursion: working with general recursive functions, without worrying about termination proofs (source).