* Deprecate "Monad.return" in favor of "pure"
* Update all included libraries to use "pure"
* Update internal code generation to remove "return"
* Remove unused AST constructor PReturn
* Update tests
This is for two reasons:
1. It is error prone, because if you edit the function, the reason for
assertion may no longer be valid, but it's no longer checked. Better to
be precise about why a function is asserted total using a combination of
assert_total, assert_smaller and (new) assert_unreachable
2. It is a very tedious maintenance burden.
Reason 1 is the good reason. Reason 2 is why I actually did this.
Not using the 'rewrite' tactic any more, but building an application of
a rewriting lemma with a predicate directly. This allows a new syntax:
rewrite [rule] using [rewrite_lemma] in [scope]
Where rewrite_lemma is any function of the right shape, so can be a
function used to rewrite dependent types rather than the default, which
is rewrite__impl.
More to do: the rewrite_lemma could be generated automatically for many
dependent types, also the predicate building needs a bit of polish, but
this already works for, e.g., rewriting vector functions.
The creation of the item could cause a collection making the pointer to the closure invalid.
Also, make the test slightly gentler to stop it from exhausting the default stack size on Windows.
