Segfault

Stream: general

[Yury G. Kudryashov]

If I add set_option old_structure_cmd true right above the definition of src#normed_ring, Lean segfaults (Linux).

[Yury G. Kudryashov]

I need normed_ring to become an old structure because I need a normed_comm_ring.

[Floris van Doorn]

I think I tried to do that too at some point:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/C*-algebras
I never ended up doing something with that.

I think the problem is that

Should I make a PR turning normed_ring (and all other structures in the algebraic hierarchy) into something that uses old_structure_cmd?

So if you turn normed_ring into and old_structure, then you should also make all structures it depends on an old_structure. (Of course, this should not cause a segfault but an error)

[Yury G. Kudryashov]

Another option is to make a mixin has_mul_comm