idris-lang/Idris-dev — pull request #745 by david-christiansen (2013-12-20 22:58:17+00:00)
Title: Add a function for dealing with absurdity

Now, if a type is known to be uninhabited, `absurd` will immediately
find the proof of uninhabitedness and apply `FalseElim` to it. This can
inhabit any type.

Example:

foo : Fin Z -> String
foo f = absurd f