Subtype polymorphism

Stream: new members

[Martin Dvořák]

Is there a way how to use a term of a subtype in place of an argument expecting a term of its parent type without having to write subtype.val in front of the term? I hope Lean has this automatic conversion (or rather, subtype polymorphism).

[Junyan Xu]

x.val or x.1 ?

[Eric Wieser]

You can write (x : the_parent_type)

[Martin Dvořák]

Junyan Xu said:

x.val or x.1 ?

OK, that is better than subtype.val x but still not what I wanted.

[Martin Dvořák]

Eric Wieser said:

You can write (x : the_parent_type)

And can it be inferred automatically? When I write the term in a position of argument of type the_parent_type please?

[Alex J. Best]

Did you try it? Works fine for me in this example

def foo : ℕ → ℕ := id
def t : { x // x * x = 4 } := ⟨2, by refl⟩
#check foo t

[Martin Dvořák]

Alex J. Best said:

Did you try it? Works fine for me in this example

def foo : ℕ → ℕ := id
def t : { x // x * x = 4 } := ⟨2, by refl⟩
#check foo t

Your code works on my computer. However, when I do an analogous thing with my types, it doesn't work. Let me play with it for a while; if I don't manage to make it work in the same way, I will create a MWE from my code.