Variable names:

m,n,k:  natural numbers
a,b,c:  types of kind Nat

When overlapping, earlier rules take precedence (as in Haskell multi-equation definitions).

{ expr } is the value of the Haskell expression expr.