Skip to content

Instantly share code, notes, and snippets.

@startling

startling/srpx.idr

Last active December 22, 2015 06:48
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save startling/6433194 to your computer and use it in GitHub Desktop.
Save startling/6433194 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
srpx.idr
data Even : Nat -> Type where
zeroIsEven : Even O
evenPlusTwoIsEven : Even k -> Even (k + 2)
twoIsEven : Even 2
twoIsEven = evenPlusTwoIsEven zeroIsEven
threeIsn'tEven : Even 3 -> _|_
threeIsn'tEven zeroIsEven impossible
threeIsn'tEven (evenPlusTwoIsEven n) impossible
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment