Coercion notation not showing

Stream: lean4

[Son Ho]

I defined a custom Coe instance below, but for some reason this coercion don't get pretty printed with the "up arrow" in goals.

import Lean

structure Foo :=
  x : Int
  y : Bool

instance : Coe Foo Int where
  coe v := v.x

example (x : Foo) (y : Int) (h : (↑x) = y) : True := by
  /-
    Goal:
    x : Foo
    y : Int
    h : x.x = y  -- HERE: I expected: h : (↑x) = y
    ⊢ True
  -/
  trivial

Does someone know where this might come from/how I could get the pretty-printing working?

[Ruben Van de Velde]

You need to add @[coe] to the function, though I'm not sure what it should be here

[Ruben Van de Velde]

attribute [coe] Foo.x, maybe

[Son Ho]

It works, thanks!