defLemma and Prop-valued classes

Stream: lean4

[Andrew Yang]

In the following snippet, the instance is a def and not a theorem. Is this intended?

class Foo : Prop where
instance foo : Foo where

#print foo
-- def foo : Foo :=
-- { }

[Floris van Doorn]

I think this is known, and it would be nice to fix. It's not that high-priority though, since there is not actually too much downside having Prop-valued things be a def. Probably it would be fine if you make an RFC for this (I think there is no one yet).

One issue this causes is that in Mathlib, if you make an alias of a Prop-valued instance, then the defLemma linter complains.

[Eric Wieser]

I think this was reported in lean4#5672, and fixed in lean4#5856

[Floris van Doorn]

Oh nice! @Sven Manthe you still had an issue with this in your project, right? It's probably fixed in the latest release candidate.

[Eric Wieser]

https://github.com/leanprover/lean4/commit/c10e4c22564d6d7d8101d82a7f41efe250ca5d92 is not in any releases yet

[Sven Manthe]

Floris van Doorn said:

Oh nice! Sven Manthe you still had an issue with this in your project, right? It's probably fixed in the latest release candidate.

I cannot remember this issue (and wasn't using much typeclass inference in the project, so this probably wasn't too relevant for my performance issues).

[Floris van Doorn]

Oh, maybe I misremembered who asked me (it was about alias triggering the defLemma linter).

[Yaël Dillies]

I did mention this at some point, but probably you are thinking of a student of yours

[Violeta Hernández]

We currently have a nolint defLemma on docs#Iff.eq, which is an alias of propext. Is this related?

[Eric Wieser]

It's related insofar as also being worth a bug report