We present an Agda library to help analyze and synthesize musical counterpoint. The tool allows expression of generic constraints in a higher-level musical language which are translated to a lower level for use both to find rule violations in existing music and to generate (using an SMT solver) new music satisfying the constraints. The tool is intended for use by musicians who need only have a basic knowledge of Agda.