How can I prove a basic inequality in dependant type language

Question

I would like to define the following function in idris, to learn how to deal with negation:

absurdity : 0 = 1 -> Void
absurdity = ?how

How can I do it ?

Could I just create an empty lambda and let the compiler figure out that this is not equal ?

Answer 1

Use impossible:

absurdity : 0 = 1 -> Void
absurdity Refl impossible