Zulip Chat Archive

Stream: mathlib4

Topic: LinearMap.CompatibleSMul

Kevin Buzzard (Jul 23 2023 at 08:18):

docs#LinearMap.CompatibleSMul this is a Type, not a Prop. What am I missing?

Kevin Buzzard (Jul 23 2023 at 09:14):

#6065 let's find out

Kevin Buzzard (Jul 23 2023 at 10:33):

Is this expected behaviour? Should I minimise?

Jireh Loreaux (Jul 23 2023 at 18:18):

Kevin, I've found bunches of these. I think they're all accidental.

Eric Wieser (Jul 23 2023 at 18:27):

We found these all the time in Lean3 too

Kevin Buzzard (Jul 24 2023 at 06:36):

Yes but in Lean 3 it was a well-known bug which I thought had been fixed

Floris van Doorn (Jul 26 2023 at 12:29):

This should probably be fixed in Lean core. In the meantime, here #6148 is a linter that checks for this and a PR that adds explicit Prop annotations in Mathlib (which I think are useful to have even if Lean would recognize these classes automatically as Props).

Last updated: Dec 20 2023 at 11:08 UTC