Zulip Chat Archive

Stream: new members

Topic: PR 4715


view this post on Zulip Damiano Testa (Oct 25 2020 at 09:48):

Dear All,

in #4175 #4715 Lean gives a linting error in finset/basic.lean. I do not think that this is a result of the changes that I made, but I am not sure. Anyway, simply changing β to γ in the statement of the lemma below is enough to fix the lint error, at least according to the #lint at the bottom of the current file. Is it ok if I simply do this, or should I perform a different change?

Thank you!

lemma nonempty.map (h : s.nonempty) (f : α  β) : (s.map f).nonempty :=
let a, ha := h in f a, (mem_map' f).mpr ha

view this post on Zulip Damiano Testa (Oct 25 2020 at 09:52):

(For added context: the lint error is

/- Checking 519 declarations (plus 152 automatically generated ones) in the current file -/

/- The `unused_arguments` linter reports: -/
/- UNUSED ARGUMENTS: -/
#print finset.nonempty.map /- argument 3: [_inst_1 : decidable_eq β] -/

/- The `decidable_classical` linter reports: -/
/- USES OF `decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF.: -/
#print finset.nonempty.map /- The following `decidable` hypotheses should be replaced with
                      `classical` in the proof. argument 3: [_inst_1 : decidable_eq β] -/

and \beta is assumed to have decidable_eq, while \gamma is not.)

view this post on Zulip Ruben Van de Velde (Oct 25 2020 at 09:53):

Is that the right PR? #4175 seems to have been merged already

view this post on Zulip Damiano Testa (Oct 25 2020 at 09:53):

Sorry, my mistake! #4715!

view this post on Zulip Damiano Testa (Oct 25 2020 at 09:53):

I will change it elsewhere as well! Thanks!

view this post on Zulip Yury G. Kudryashov (Oct 25 2020 at 09:58):

There is a [decidable_eq] assumption in variables in this section. While finset.image needs decidable_eq on the codomain, finset.map doesn't need it. I suggest that you move your lemma to the section with lemmas about finset.map or choose a type variable without [decidable_eq] assumption.

view this post on Zulip Damiano Testa (Oct 25 2020 at 10:01):

Yury G. Kudryashov said:

There is a [decidable_eq] assumption in variables in this section. While finset.image needs decidable_eq on the codomain, finset.map doesn't need it. I suggest that you move your lemma to the section with lemmas about finset.map or choose a type variable without [decidable_eq] assumption.

I moved the lemma (with the target type called \beta) at the end of the previous section (map). Everything seems to still work and lint gives no errors. Is this preferable to renaming \beta to \gamma ?

view this post on Zulip Ruben Van de Velde (Oct 25 2020 at 10:06):

It sounds like a good idea in general to keep everything about map together

view this post on Zulip Damiano Testa (Oct 25 2020 at 10:07):

Ok, I will move the lemma nonempty.map to the previous section then and push again the change. Hopefully, the PR will pass all the tests!

Thank you very much for your help!


Last updated: May 16 2021 at 05:21 UTC