Sholdn't `well_founded.recursion` be a `def`?

Stream: general

[Anne Baanen]

well_founded.recursion in core returns a Sort, but is declared as a lemma. Shouldn't it be a def instead?

[Floris van Doorn]

Yes it should. Ideally we also prove a beta rule for it.
At some point we should try to make the linter happy for the core library. This is caught by the linter:

import tactic.lint
#lint_all only def_lemma

[Anne Baanen]

lean#503