## Stream: new members

### Topic: Can't find coe

#### Fox Thomson (Jul 22 2020 at 13:22):

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 (Jul 22 2020 at 14:34):

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

#### Scott Morrison (Jul 22 2020 at 14:35):

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

Last updated: May 15 2021 at 23:13 UTC