Prop class

Stream: general

[Reid Barton]

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]

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

[Johan Commelin]

My impressions was about 86.4%

[Johan Commelin]

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

[Johan Commelin]

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.

[Miguel Raz Guzmán Macedo]

Got it...

[Floris van Doorn]

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.