I must be some sort of idiot. Here comes the third try:

<code>

# This is a comment.

Nat : Type;
0 : Nat;
succ : Nat > Nat;

#!
+ : Nat > Nat > Nat
  = $0? m! m
  | $succ n? m! + n (succ m);
!#

+ m = $0? m
    | $succ n! + (succ m) n;

List : Nat > Type > Type;
nil : t < List 0 t;
cons : n < t < t > List n t > List (succ n) t;

sum : n < List n Nat > Nat
    = $cons x xs? + x (sum xs)
    | $nil! 0;

map : n < a < (a > a) > List n a > List n a
    = f! $nil? nil
       | $cons x xs! cons (f x) (map f xs);

(foldr : n < a < b < (a > b > b) > b > List n a > b)
       f z = $nil? z
           | $cons x xs! f x (foldr f z xs);

(foldr1 : n < a < b < (a > b > b) > b > List (succ n) a > b)
        f z ($cons x xs) = foldr f x xs;

foldl f z = $nil? z
          | $cons x xs! foldl f (f z x) xs;

foldl1 f ($cons x xs) = foldl f x xs

Matrix : Nat > Nat > Type > Type

mkMatrix = m < n < t < List m (List n t)

mul : a < b < c < t < Matrix a b t > Matrix b c t > Matrix a c t
    = #not implemented.

</code>

the <code> tags aren't even necessary, are they?