Skip to content

Instantly share code, notes, and snippets.

@msmorgan

msmorgan/Ter.idr

Created November 20, 2017 03:34
Show Gist options
  • Save msmorgan/36cafdbbf0f56a46bf2fb5a00fd3de4d to your computer and use it in GitHub Desktop.
Save msmorgan/36cafdbbf0f56a46bf2fb5a00fd3de4d to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Ter.idr
data CloserToZero : Integer -> Integer -> Type where
CTZ : So (x * x < y * y) -> CloserToZero x y
CTZInj : CloserToZero x y -> So (x * x < y * y)
CTZInj (CTZ oh) = oh
closerToZero : (x, y : Integer) -> Dec (CloserToZero x y)
closerToZero x y with (x * x < y * y) proof prf
closerToZero x y | True = Yes (CTZ (rewrite sym prf in Oh))
closerToZero x y | False = No (absurd . the (So False) . rewrite prf in CTZInj)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment