Zulip Chat Archive

Stream: new members

Topic: linter error

Matias Heikkilä (Apr 17 2022 at 15:07):

any idea how to solve linter error?

/- INCORRECT DEF/LEMMA: -/
***  /- is a lemma/theorem, should be a def -/

Henrik Böving (Apr 17 2022 at 15:10):

Can you show us the entire code?

Matias Heikkilä (Apr 17 2022 at 15:10):

sure just a sec

Eric Wieser (Apr 17 2022 at 15:13):

Do what the message tells you; replace the word "lemma" or "theorem" with the word "def"

Eric Wieser (Apr 17 2022 at 15:14):

The line above or below in that error message (which you didn't include in your Zulip message!) should tell you which line to do that replacement on

Matias Heikkilä (Apr 17 2022 at 15:18):

https://github.com/leanprover-community/mathlib/pull/13487/files

so here's the diff (sorry it's still very WIP)

Matias Heikkilä (Apr 17 2022 at 15:19):

What I would like to do is to define an universal property and then show that it gives an unique space (up to an isomorphism)

Matias Heikkilä (Apr 17 2022 at 15:21):

I'm not sure if stone_cech_universal_unique should intuitively be a def so I suspect I've done this wrong somehow

Eric Wieser (Apr 17 2022 at 18:24):

It should be a def because ≃ₜ (docs#homeomorph) carries data

Last updated: Dec 20 2023 at 11:08 UTC