Zulip Chat Archive

Stream: general

Topic: Prop class


view this post on Zulip 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 := (...)?

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 12 2019 at 19:35):

My impressions was about 86.4%

view this post on Zulip Johan Commelin (Oct 12 2019 at 19:35):

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

view this post on Zulip 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.

view this post on Zulip Miguel Raz Guzmán Macedo (Oct 12 2019 at 19:38):

Got it...

view this post on Zulip 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