Skip to content

Instantly share code, notes, and snippets.

@hoelzro

hoelzro/Even-add.idr

Created April 18, 2018 17:34
Show Gist options
  • Save hoelzro/c84c443a9d0b80145b10e3769269c9a4 to your computer and use it in GitHub Desktop.
Save hoelzro/c84c443a9d0b80145b10e3769269c9a4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Even-add.idr
data Even : (n : Nat) -> Type where
MkEven : (half_n : Nat) -> Even (half_n + half_n)
oddIsOdd : Even (S (n + n)) -> Void
oddIsOdd _ impossible
{-
Type checking ./Even.idr
Even.idr:5:12-21:
|
5 | oddIsOdd _ impossible
| ~~~~~~~~~~
oddIsOdd _ is a valid case
-}
Raw
Even-multiply.idr
data Even : (n : Nat) -> Type where
MkEven : (half_n : Nat) -> Even (half_n * 2)
oddIsOdd : Even (S (n * 2)) -> Void
oddIsOdd _ impossible
-- compiles fine
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment