Zulip Chat Archive

Stream: new members

Topic: Can't find coe

view this post on Zulip 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 :=

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

view this post on Zulip 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.

view this post on Zulip 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