Extending a class with two classes

Stream: new members

[Mukesh Tiwari]

I have a definition of class meet_semilattice (A : Type u) (R : A -> A -> Prop) (meet : A -> A -> A) extends partial_order A R and
class join_semilattice (A : Type u) (R : A -> A -> Prop) (join : A -> A -> A) extends partial_order A R, and Now I am trying to extend these two classes to
class lattice (A : Type u) (R : A -> A -> Prop) (meet : A -> A -> A) (join : A -> A -> A) extends
(meet_semilattice A R meet)(join_semilattice A R join) by following https://github.com/leanprover/lean/blob/master/library/init/algebra/group.lean#L33

[Mukesh Tiwari]

But I am getting this error "Invalid 'structure' header, field 'to_partial_order' from 'Ordering.join_semilattice' has already been declared

[Mukesh Tiwari]

https://gist.github.com/mukeshtiwari/6d40904d33911e46d342d194c1771a5b

[Patrick Massot]

You could have a look at how all this is done in the standard library: https://github.com/leanprover-community/mathlib/blob/master/src/order/lattice.lean

[Patrick Massot]

If you want something closer to what you try, you can change meet_semilattice, join_semilattice and lattice to take [partial_order A R] as a parameter. Of course you'll also need to find other names for H₁ etc in order to avoid name clashes.

[Patrick Massot]

But the setup in mathlib will probably be much more convenient.

[Mukesh Tiwari]

Thanks for the help Patrick.

[Kevin Buzzard]

You might also want to use the "old structure command" -- ("old" as in "the way it used to be done by default", rather than "deprecated"): see https://github.com/leanprover/lean/wiki/Refactoring-structures . In that document, "the current approach" is what is now called the old approach. For lattices this might be what you want. set_option old_structure_cmd true

[Mukesh Tiwari]

Thanks Kevin.