Infer kinds are unsupported

Stream: mathlib4

[Moritz Doll]

What should I do about this error from mathport?

/- ./././Mathport/Syntax/Translate/Command.lean:379:30: infer kinds are unsupported in Lean 4: #[`abv_nonneg] [] -/

[Ruben Van de Velde]

Never seen that. Does it break anything?

[Moritz Doll]

nope

[Moritz Doll]

(except for the 100 char linter)

[Ruben Van de Velde]

Maybe it's about the [] in the mathlib3 declaration? I never understood what those were for either :)

[Eric Rodriguez]

So it's about setting some things to implicits, I don't know how to describe it but the answer is kinda "look at docs#countable vs docs4#Countable and the next few lines"

[Eric Rodriguez]

This has bit me before and should be written in the wiki, I would do it but I'm a bit under the weather

[Mario Carneiro]

the effect of the [] in src#is_absolute_value.abv_nonneg is to make the f argument explicit. Lean 4 does not support this annotation, so if you take the definition that mathport gives you then f will be implicit.

[Mario Carneiro]

I don't think there is any principled reason for the removal in lean 4, except for an optimistic hope that it is a rarely used feature with a weird syntax and we can get by without it

[Jireh Loreaux]

What about when the structure field is data (e.g., docs#bornology.cobounded)? If I follow the method in docs4#Countable, I would have a structure field Bornology.cobounded' where the α is implicit and a def following it Bornology.cobounded with α explicit. Surely we don't want both floating around though. So how do I handle this?