cslib linkifier

Stream: CSLib

[Snir Broshi]

Eric Wieser said:

The total number of models after CSLib#357 is still one.

Huh, there's a different linkifier for cslib# and CSLib#. Can you delete the latter and make the former case-insensitive? The link you sent is currently broken

[Shreyas Srinivas]

Snir Broshi said:

Eric Wieser said:

The total number of models after CSLib#357 is still one.

Huh, there's a different linkifier for cslib# and CSLib#. Can you delete the latter and make the former case-insensitive? The link you sent is currently broken

Different topic please

[Notification Bot]

2 messages were moved here from #CSLib > Lightweight algorithms in CSLib :Cslib#275 by Chris Henson.

[Chris Henson]

It's not something specifically added, it's using the default to to the leanprover-community scope when another linkifier doesn't exist

[Snir Broshi]

So can we make the linkifier case-insensitive to avoid the default no matter how people case it?

[Chris Henson]

I'm not sure who to ping, but yes, that seems a reasonable change (to the cslib linkifier)

[Snir Broshi]

Well that's kind of why I commented on the original thread, I assumed Eric has permissions to fix it and I would only send 1 off-topic message