auto-bound implicits

Stream: lean4

[Sebastian Ullrich]

By the way, I would be interested to hear about your reasons for preferring to turn them off. This feature is still somewhat in an experimentation phase.

[Horatiu Cheval]

Basically to protect myself from my own negligence. I just had a constructor using some x intended as an autobound variable, but actually I had in another imported file some def x := ..., so the x was actually referring to that rather than being a variable. And because of this I spent some time not understanding why an induction case complained about a wrong number of arguments.

[Horatiu Cheval]

But I think it's a nice feature and can make code more readable in some situations, but requires some discipline on the part of the programmer which I just wanted to skip when just playing around and doing experiments

[Sebastian Ullrich]

Hah, that is exactly the anticipated failure case, yes. Semantic highlighting should warn you about it, but you first have to be aware of it doing that of course.

[Sebastian Ullrich]

Perhaps we should try to find a more noticeable highlighting for implicits specifically image.png

[Horatiu Cheval]

Oh, I see now. Yes, I certainly didn't notice or think of the difference in highlighting in that moment :)