Do two passes through delayed elaborators (it's impossible to predict
dependency order). Possibly this should keep going as long as it's
making progress? I'll consider that later.
A few people have reported issues that this won't build with Idris 1.3.1, which it won't. There's a note in INSTALL.md, but it's clearly not prominent enough! I will do a new release soon, but it does take time to do it properly!
Surprisingly == on Nat in the Idris prelude is linear! So shortcut that
by converting to an Integer first. Also a couple of small things in the
evaluator that have a small but noticeable effect when environments are
big.
