Zulip Chat Archive
Stream: general
Topic: mul and add type class hierarchies
Sean Leather (Oct 04 2018 at 07:53):
I'm curious why we have two nearly duplicate type class hierarchies – multiplicative and additive – in Lean. It seems like it would be better to have the type classes be parameterized by the binary operator instead of inheriting the operator. I suppose there are technical/practical problems here which led to the current design.
Johan Commelin (Oct 04 2018 at 07:54):
Yes. You are right. I'll search for the discussion. 1 sec
Johan Commelin (Oct 04 2018 at 07:56):
Johan Commelin (Oct 04 2018 at 07:56):
@Sean Leather :up:
Chris Hughes (Oct 04 2018 at 07:57):
Also https://github.com/leanprover/lean/wiki/Refactoring-structures
Sean Leather (Oct 04 2018 at 08:08):
Also https://github.com/leanprover/lean/wiki/Refactoring-structures
I've tried to read that before and my eyes glazed over every time.
Last updated: Dec 20 2023 at 11:08 UTC