defining notations and structures simultaneously

Stream: lean4

[Jason Gross]

Is there a way to do something like

structure Cat where
  Obj : Type
  Hom : Obj → Obj → Type
  infix " ~> " => Hom
  id : ∀ {a}, a ~> a

?

[Sebastian Ullrich]

There was in Lean 3, but not yet in Lean 4. However, there is a workaround:

section
set_option hygiene false
local infix " ~> " => Hom

structure Cat where
  Obj : Type
  Hom : Obj → Obj → Type
  id : ∀ {a}, a ~> a
end

infix " ~> " => Cat.Hom
#check fun a b => a ~> b