Zulip Chat Archive

Stream: new members

Topic: Type alias without creating a new type


Ryan Greenblatt (Nov 15 2021 at 18:56):

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 (Nov 15 2021 at 18:56):

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

Heather Macbeth (Nov 15 2021 at 19:08):

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

Heather Macbeth (Nov 15 2021 at 19:08):

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

Last updated: Dec 20 2023 at 11:08 UTC