Can't find coe

Stream: new members

[Fox Thomson]

Lean doesn't seem to be able to use the coe I have defined in the following code. I have tried explicitly using lifts but that doesn't seem to be working either.

inductive impartial_pgame : Type (u+1)
| mk : ∀ α : Type u, (α → impartial_pgame) → impartial_pgame

def impartial_pgame_to_pgame : impartial_pgame → pgame
| (mk m M) := pgame.mk m m (λ i, (M i).impartial_pgame_to_pgame) (λ i, (M i).impartial_pgame_to_pgame)
@[instance] def imartial_pgame_to_pgame_coe : has_coe impartial_pgame pgame :=
⟨ impartial_pgame_to_pgame ⟩

def subsequent (G H : impartial_pgame) : Prop := pgame.subsequent G H

[Scott Morrison]

I think you'll have to post a #mwe to get help with this; I don't even remember a pgame.subsequent.

[Scott Morrison]

(But general, if unsolicited advice: don't bother making coercions... They're nice when they work, but difficult, and best left for later.)