## Stream: general

### Topic: Prop class

#### Reid Barton (Oct 12 2019 at 18:04):

If we have class C a : Prop := (...), and then instance foo : C bar := (...), I guess Lean treats foo as a def not a lemma, right?
Is there ever an argument for writing @[instance] lemma foo : C bar := (...)?

#### Miguel Raz Guzmán Macedo (Oct 12 2019 at 19:31):

How much breakage of user code that doesn't use internals is expected in the lean 3 -> lean 4 transition?

#### Johan Commelin (Oct 12 2019 at 19:35):

No seriously... I think we shouldn't expect any compatibility

#### Johan Commelin (Oct 12 2019 at 19:36):

But some people on the chat, who are a lot more skilled than I am, might be able to convert huge bunches of code using fancy metaprogramming trick plus Perl regexes.

Got it...

#### Floris van Doorn (Oct 12 2019 at 19:41):

If we have class C a : Prop := (...), and then instance foo : C bar := (...), I guess Lean treats foo as a def not a lemma, right?
Is there ever an argument for writing @[instance] lemma foo : C bar := (...)?

This is correct. And all instances also have a greater transparency than the default (semireducible).

Maybe there is sometimes an argument for @[instance] lemma, but I don't think it matters very much when you use def instead of lemma (the other way around is bad). Note: for #sanity_check I explicitly omit everything tagged with @[instance] from the lemma/def check.

Last updated: May 14 2021 at 06:16 UTC