Zulip Chat Archive
Stream: mathlib4
Topic: !4#3169
Jeremy Tan (Mar 29 2023 at 09:27):
!4#3169 There are quite a few definitions in here I had to make noncomputable. Should I just leave it like this or not?
Jeremy Tan (Mar 29 2023 at 09:33):
Also should this file be renamed TwopCat to match RelCat, QuivCat, etc. (and Pointed to PointedCat, etc.)?
Eric Wieser (Mar 29 2023 at 09:39):
It looks like docs4#Prod.Bipointed is noncomputable due to alias being weird?
Notification Bot (Mar 29 2023 at 10:25):
2 messages were moved from this topic to #mathlib4 > alias is noncomputable by Eric Wieser.
Yaël Dillies (Mar 29 2023 at 10:28):
Twop doesn't conflict with an existing name so I don't see why it should be renamed.
Yaël Dillies (Mar 29 2023 at 10:28):
Quiv should remain Quiv too
Last updated: Dec 20 2023 at 11:08 UTC