trouble defining has_coe instance

Stream: general

[Bernd Losert]

For some reason, this doesn't work:

import tactic
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter
open has_sup

variable a : Type*

structure convergence_space (a : Type*) :=
(converges : filter a -> a -> Prop)

attribute [class] convergence_space

open convergence_space

structure kent_convergence_space (a : Type*) extends convergence_space a :=
(kent_converges : forall {x} {l}, converges l x -> converges (sup l (pure x)) x)

attribute [class] kent_convergence_space

open kent_convergence_space

instance has_coe : (kent_convergence_space a) (convergence_space a) := {
  coe := fun p, p.to_convergence_space,
}

I can't figure out what I am doing wrong here.

[Adam Topaz]

@Bernd Losert Do you know about unicode input? (not really related to your issue)

[Bernd Losert]

Yes. I am avoiding it at the moment until I get a better set up.

[Adam Topaz]

Ok, just checking.

[Adam Topaz]

The issue here is that you did not write has_coe : has_coe _ _

[Adam Topaz]

Instead you wrote has_coe : _ _

[Adam Topaz]

Also, I think the name has_coe will cause issues. I suggest replacing the -3 line with

instance : has_coe (kent_convergence_space a) (convergence_space a) := {

and see whether lean is able to automatically generate a good name for you

[Bernd Losert]

A crap. It's the colon that is in the wrong spot. Duh!

[Bernd Losert]

Thanks for pointing that out.

[Adam Topaz]

No problem!