Coda's website

Here is a fun example of the proof of the commutativity of addition

            type zero = Invisible1_
            type 'a succ = Invisible2_ of 'a  
              
            type _ is_nat =
              | IsZ : zero is_nat
              | IsS : 'a is_nat -> 'a succ is_nat
            
            type (_,_,_) add =
              | AddZ : (zero, 'b, 'b) add
              | AddS : ('a, 'b, 'c) add -> ('a succ, 'b, 'c succ) add
              
            type (_,_) eq =
              | Refl : ('a, 'a) eq
                    
            let rec add_Z : type x. x is_nat -> (x, zero, x) add = function
              | IsZ -> AddZ
              | IsS n -> AddS (add_Z n)
            
            let rec add_succ_r : type a b c. (a,b,c) add -> (a,b succ,c succ) add = function
              | AddZ -> AddZ
              | AddS p -> AddS (add_succ_r p)
                            
            let rec add_comm : type a b c.
              a is_nat -> b is_nat -> (a,b,c) add -> (b,a,c) add
              = fun a b p ->
                match a, p with
                | IsZ, AddZ ->
                    add_Z b
                | IsS a', AddS p' ->
                    add_succ_r (add_comm a' b p')