cc

Stream: mathlib4

[Johan Commelin]

Is it useful to remove cc from mathlib? Or should we not even try?

[James Gallicchio]

I've been looking into re-implementing cc in lean4. It definitely needs to be written eventually, since it's pretty fundamental for many CS applications, so I don't think it's worth removing uses from mathlib?

[Johan Commelin]

But it's crucial to make mathport happen. So there we should either port it in the near future, or (temporarily) remove it from mathlib.

[Gabriel Ebner]

There are surprisingly few uses of cc in mathlib. Many occurrences of the word cc are hypothesis names.

[Gabriel Ebner]

I think it's relatively straightforward to replace them during porting. Either we have cc by then or not, it's easy enough to fix. I wouldn't worry right now.

[Johan Commelin]

Ok, understood