# It's easy to say something that's false, but
# it had better be hard to prove something that's false.
# Programs correspond to proofs. That's why it's
# hard to come up with an example of the False type.

((hang:False) be (\@b->b))

# hang is a built-in term of type False.  Just as False must not be provable,
# evaluation of the term 'hang' must not finish.
# In the current implementation, rather than hanging, it aborts.