Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/gist:4994631

Last active December 13, 2015 23:49
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 david-christiansen/4994631 to your computer and use it in GitHub Desktop.
Save david-christiansen/4994631 to your computer and use it in GitHub Desktop.
Download ZIP
Simple predicate
Raw
gistfile1.txt
module PropDemo
data GreaterThanTwo : Nat -> Type where
threeOK : GreaterThanTwo 3
moreOK : GreaterThanTwo n -> GreaterThanTwo (S n)
total sumGreater : GreaterThanTwo n -> GreaterThanTwo m -> GreaterThanTwo (n + m)
sumGreater threeOK mOK = moreOK (moreOK (moreOK mOK))
sumGreater (moreOK nOK') mOK = moreOK (sumGreater nOK' mOK)
@david-christiansen
Copy link
Author

This is a simple proof shown in an impromptu IRC tutorial session on dependent types and representing predicates.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment