How to deal with equalities over `BitVec.cast`

Stream: general

[Ayhon]

I've noticed that my question should have been posted over here, and not in #new members > How to deal with equalities over `BitVec.cast`, which by its description is a channel meant for introductions. However I'm not able to move the conversation to a different channel. If someone could do it in my stead I'd be grateful.

[Notification Bot]

Ayhon has marked this topic as resolved.

[Notification Bot]

Ayhon has marked this topic as unresolved.

[Patrick Massot]

The new members channel was indeed intended for introductions, but people immediately misinterpreted it as being intended for beginners questions, and then a tradition was established. I guess we could modify the channel description to match its actual use.

[Yaël Dillies]

Patrick, in four years of living on Zulip, this is the first time I am hearing this!

[Edward van de Meent]

you mean this legend of the original purpose of #new members, or the fact that channel descriptions can be changed?

[Yaël Dillies]

The legend of the original purpose

[Patrick Massot]

I don't know why you call this a legend. It is very clearly explained in the channel description.

[Edward van de Meent]

i only meant it in the "story" sense, not in the "fictional" sense

[Ayhon]

Patrick Massot said:

The new members channel was indeed intended for introductions, but people immediately misinterpreted it as being intended for beginners questions, and then a tradition was established. I guess we could modify the channel description to match its actual use.

Yes, I had that misconception as well, but then saw the channel description and wasn't sure if I should move the topic or not. Not that I could do so in any case.

It seems like the original topic has gathered the most attention, I think I can consider this question solved, the conclusion being "it's a bit annoying to do rewritings with dependent types"

[Yaël Dillies]

Patrick Massot said:

I don't know why you call this a legend. It is very clearly explained in the channel description.

Depends on how you interpret it. For me, "onboarding" means more than replying to a single message saying "hello" :sweat_smile: