Type equality

Stream: new members

[Keeley Hoek]

Is it possible to decide whether two types are equal?

[Kenny Lau]

no

[Keeley Hoek]

That makes me sad

[Kenny Lau]

local attribute [instance] classical.dec

[Keeley Hoek]

Cheers, but I wanted to use it in a program

[Keeley Hoek]

Instead I think I'm going to have to concoct some user_notation trickery to get the same syntax

[Kevin Buzzard]

I've heard it said here that even nat = int is undecidable

[Kenny Lau]

independent, even

[Abhimanyu Pallavi Sudhir]

I've heard it said here that even nat = int is undecidable

How exactly are we defining equality of types?

[Chris Hughes]

As defined in Lean. If you separately define two inductive types of the same size, their equality will be independent.

[Keeley Hoek]

I guess the lesson is to stay in expr-land if you're trying to do something programmatically like this (e.g. either its a expr.const `bool [] or its not)

[Mario Carneiro]

Well, it depends on what you mean. That will not get id bool = bool

[Keeley Hoek]

sure yep