Zulip Chat Archive
Stream: general
Topic: Changing the notation for Matrix.mul
Eric Wieser (Aug 10 2023 at 10:36):
Jireh Loreaux said:
Can't we just use
*for matrix multiplication now? Have we tried it yet, or are we worried it's just going to cause elaboration hell?
Eric Wieser (Aug 11 2023 at 08:28):
Eric Wieser said:
After adding @[default_instance], CI is happy with this!
Eric Wieser (Aug 11 2023 at 16:54):
A really trivial spin-off: #6522
Notification Bot (Aug 11 2023 at 20:53):
A message was moved here from #lean4 > .·⬝ [rant] by Eric Wieser.
Eric Wieser (Aug 11 2023 at 20:56):
@Kyle Miller, do you think it's possible/sensible to write a custom elaborator for matrix multiplication to help with some of the weirdness in that PR? In particular, something that says "oh, you're multiplying Matrix ?m ?n ?A and Matrix ?l ?o ?B, let me unify ?A = ?B and ?n = ?l for you before continuing"
Anatole Dedecker (Aug 11 2023 at 20:58):
Isn't that the point of unification hints? Sorry if I'm speaking nonsense
Last updated: Dec 20 2023 at 11:08 UTC