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?