We present Music Tools, an Agda library for analyzing and synthesizing music. The library uses dependent types to simplify encoding of music rules, thus improving existing approaches based on simply typed languages. As an application of the library, we demonstrate an implementation of first-species counterpoint, where we use dependent types to constrain the motion of two parallel voices.
各種検索
サポート
ヘルプ