Type alias without creating a new type

Stream: new members

[Ryan Greenblatt]

I'd like to be able to define some shorthand for a type. For instance something like:

def alias_nat := ℕ

However, this isn't actually an alias, this is a new type. For example, it doesn't share all of the same type class instances.

Is there syntax for actual aliases? If not, is there a way to derive all type classes? (I can't figure out how to even derive multiple type classes with @[derive _].

[Ryan Greenblatt]

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20use.20a.20type.20alias.20without.20breaking.20typeclass.20synthesis

[Heather Macbeth]

@Ryan Greenblatt See docs#normed_space.dual for an example

[Heather Macbeth]

/-- The topological dual of a seminormed space `E`. -/
@[derive [inhabited, semi_normed_group, semi_normed_space 𝕜]] def dual := E →L[𝕜] 𝕜