Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Anne Baanen (Nov 18 2020 at 09:55):

lean#503


Last updated: May 12 2021 at 23:13 UTC