Zulip Chat Archive

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):


Last updated: Aug 03 2023 at 10:10 UTC