## Stream: general

### Topic: Sholdn't well_founded.recursion be a def?

#### Anne Baanen (Nov 17 2020 at 09:33):

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

#### Floris van Doorn (Nov 17 2020 at 20:04):

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 (Nov 18 2020 at 09:55):

lean#503

Last updated: May 12 2021 at 23:13 UTC