Riley Cat WreckedAvent
jonschoning
/ add-require-x-less-than-y.idr
Last active
August 24, 2016 19:11
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |