Zulip Chat Archive

Stream: general

Topic: mul and add type class hierarchies


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:54):

Yes. You are right. I'll search for the discussion. 1 sec

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:56):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/additive.20group.20homs/near/127064577

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:56):

@Sean Leather :up:

view this post on Zulip Chris Hughes (Oct 04 2018 at 07:57):

Also https://github.com/leanprover/lean/wiki/Refactoring-structures

view this post on Zulip 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: May 14 2021 at 22:15 UTC