Twelf description of music harmony presented in http://dreixel.net/research/pdf/fmmh.pdf

western-harmony.lf

root : type.
i : root.
ii : root.
iii : root.
iv : root.
v : root.
vi : root.
vii : root.

v/ : root -> root -> type.
v/i   : v/ i v.
v/ii  : v/ ii vi.
v/iii : v/ iii vii.
v/iv  : v/ iv i.
v/v   : v/ v ii.
v/vi  : v/ vi iii.
v/vii : v/ vii iv.

class : type.
maj : class.
min : class.
dom7 : class.

nat : type.
z : nat.
s : nat -> nat.

degree : root -> class -> nat -> type.
base : {R} {C} degree R C z.
cons : {R} {C}
  v/ R R' -> degree R' dom7 N -> degree R C z
    -> degree R C (s N).

dominant : nat -> type.
fin : degree v maj _ -> dominant z.
sub : degree iv maj _ -> dominant N -> dominant (s N).

phrase : nat -> type.
ton : phrase z.
dom : dominant N -> phrase (s N).

piece : type.
nil : piece.
; : piece -> phrase _ -> piece.
%infix left 1 ;.

%solve chord : degree v maj (s z).
foo : piece =
          nil ; ton ; (dom (fin chord)) ; ton.

%solve x : dominant (s (s z)).