Having trouble converting Nat to generic type

Stream: new members

[Colin Jones ⚛️]

Hi, I've been having issues with this particular line of code:

import Mathlib

variable (n m : ℕ)

def Y2 [OfNat α m]: α := (m : α)

Does anyone know why this doesn't work?

[Damiano Testa]

Does it work without saying that α is a Type?

[Kyle Miller]

OfNat is meant to be used to give literal numbers an interpretation, and it's not meant to be a general coercion.

You can do

def Y2 [Coe Nat α] : α := (m : α)

or use some algebraic typeclass that provides such a coercion and do for example

def Y2 [Ring α] : α := (m : α)

[Colin Jones ⚛️]

Does the Coe Nat stand for coercion?

[Colin Jones ⚛️]

Thank you!