Zulip Chat Archive

Stream: general

Topic: derive instances

Bernd Losert (Apr 26 2022 at 21:12):

Say I have def MyNat := nat. Is there a macro that will derive instsances for e.g. has_add from the nat instance?

Yaël Dillies (Apr 26 2022 at 21:13):

@[derive has_add] def MyNat := nat

Bernd Losert (Apr 26 2022 at 21:22):

Thanks. If I just want MyNat to be an "alias" to nat, how do I define it?

Bernd Losert (Apr 26 2022 at 21:22):

Should I just define it as syntax?

Yaël Dillies (Apr 26 2022 at 21:25):

abbreviation MyNat := nat

Bernd Losert (Apr 26 2022 at 21:35):

Cool. Thanks.

Last updated: Dec 20 2023 at 11:08 UTC