Skip to content

Instantly share code, notes, and snippets.

@kojiromike

kojiromike/gist:a2286d74b480818e06e5

Created July 24, 2014 16:55
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 kojiromike/a2286d74b480818e06e5 to your computer and use it in GitHub Desktop.
Save kojiromike/a2286d74b480818e06e5 to your computer and use it in GitHub Desktop.
Download ZIP
even function from idris tutorial
Raw
gistfile1.idr
even : Nat -> Bool
even Z = True
even (S k) = odd k
where
odd Z = False
odd (S k) = even k
@kojiromike
Copy link
Author

From http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf This is a good example of the elegance of FP. We define a function even that takes a natural number and returns a boolean. If the argument is 0 (Z), we assume the result is True. If the argument is a successor to a natural number k, we assume the result is odd k, where odd of 0 is False and odd of a successor to (another) k is even k. So the entire meaning of even and odd are reduced down to the meaning of even and odd of 0 and its successors.

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