Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and well-founded recursion and derives useful proof principles for demonstrating properties about them. In this presentation we give an overview of several components of Equations through the help of an example that will serve as a main thread during the session. First of all, we describe the splitting tree, the intermediate data structure used to represent a function defined by Equations. We also explain how recursive definitions are handled by Equations. Finally, we present a mostly independent module that allows to simplify equalities generated to perform dependent pattern-matching on a variable.