Lifting structures to aliased types

Stream: new members

[Kevin Sullivan]

Hi everyone, what's the standard way to lift structures/operations associated with a type, Q, to a new new type, obtained by def R := Q?

[Kevin Buzzard]

You can use @[derive foo] to lift the typeclass instance foo from Q to R (write it just before the definition of R), and @[derive [foo,bar,baz]] if you want to lift more than one.

[Kevin Sullivan]

Kevin Buzzard said:

You can use @[derive foo] to lift the typeclass instance foo from Q to R (write it just before the definition of R), and @[derive [foo,bar,baz]] if you want to lift more than one.

Thank you, Kevin. --K