Lifting instances from other types

Stream: new members

[Fingy Soupy]

I am defining a small wrapper type around another type and I would like my new type to "inherit" all of the instances of the other type
For example,

structure nat_plus :=
(v : nat)
instance : has_lift nat nat_plus := ⟨nat_plus.mk⟩
instance : linear_order nat_plus := ↑nat.linear_order -- Does not work

Here I have wrapped the nat type and would like my new type to use nat's linear_order. Is there a way to do this using coe/lift and without having to wrap each individual field in every instance I would like to copy over?

[Eric Wieser]

There are helpers like docs#function.injective.add_comm_monoid

[Eric Wieser]

And docs#linear_order.lift

[Fingy Soupy]

This is perfect thanks,
Is there a reason there is no complete_lattice.lift?

[Rémy Degenne]

There is docs#function.injective.complete_lattice

[Fingy Soupy]

Thanks! :) I guess I was looking in the wrong place

[Eric Wieser]

There's an open issue about standardizing the names