Anonymous methods

[Aurel300]

Along the same lines as #894, it would be nice to be able to emit an anonymous method when that method is only a lemma that is not meant to be called.

method(x: Ref)
    requires ...
{
    assert ...
}