jonschoning

import Data.String

                                                  -- takes two integers, and a proof that x < y, and yields an integer
add : 
  (x : Integer) -> 
  (y : Integer) -> 
  (prf : x < y = True) ->                         -- require a proof that that x < y
  Integer
add x y prf = x + y