with top with bottom

Stream: new members

[Huỳnh Trần Khanh]

this is probably separate from the egregiousness issue so I'm creating a new thread. why are their definitions... the same?

[Eric Wieser]

Note that multiplicative X, additive X, and order_dual X are also "the same".

[Eric Wieser]

However, just because things are the same after you unfold them doesn't mean they're not worth having. What's relevant here is that typeclass search does not unfold them, so with_top and with_bot have different typeclass instances associated with them than option does.

[Huỳnh Trần Khanh]

so they are like... newtypes?

[Huỳnh Trần Khanh]

or am i missing something

[Damiano Testa]

For me, the example below cleared some of the doubts that I had.

If you want to describe the reals to which you add (+infinity), you can do it in two stages.

1. Add a new element to the reals;
2. declare the new element to be bigger than anything else.

Similarly, if you want to describe the reals to which you add (-infinity), you can do it in two stages.

1. Add a new element to the reals;
2. declare the new element to be smaller than anything else.

The two constructions begin with the same first step. However, if you know where you are headed, it makes sense to call the first new element (+infinity) and the second one (-infinity). You let Lean know about this by giving different names to the same thing.

[Huỳnh Trần Khanh]

hmm okay so this sounds like newtype to me

how does the alias command work then? can an alias have different typeclass instances than the original type?

[Damiano Testa]

I have only seen alias used for assigning a different name to an existing lemma. docs#tactic.alias.alias_attr

[Kevin Buzzard]

If you def X := nat then X doesn't have any of the typeclass instances of nat and you can add new instances to X which will not be picked up by nat. Conversely there's some @[derive] trickery which you can use to pull instances over from nat to X if you want them there.