field notation for instances

Stream: lean4

[Alexandre Rademaker]

Is there any alternative syntax for Proponent.id c? I tried c.id, but it doesn't work.

class Proponent (a : Type → Type → Type) where
  id {α β : Type} : a α β → α
  prefs {α β : Type} : a α β → List β

class Receptor (a : Type → Type → Type) where
  id {α β : Type} : a α β → β
  capacity {α β : Type} : a α β → Nat
  prefs {α β : Type} : a α β → List α

def test {C P α β} [ToString α] [ToString β] [Proponent C] [Receptor P]
  (c : C α β) (p : P α β)
  : String :=
  let a := Proponent.id c  -- c.id didn't work
  let b := Receptor.id p   -- p.id didn't work
  s!"{a}{b}"

[Kenny Lau]

@Alexandre Rademaker dot notation (c.id) only works if c has type Proponent ...

[Kenny Lau]

so there won't be a shorter syntax

[Alexandre Rademaker]

It doesn't add too much for me, but I noticed I can also add a name to the instance:

def test {C P α β} [ToString α] [ToString β]
  [m : Proponent C] [n : Receptor P]
  (c : C α β) (p : P α β)
  : String :=
  let a := m.id c
  let b := n.id p
  s!"{a}{b}"

[Kenny Lau]

have you considered making them structure instead of class

[Alexandre Rademaker]

This is my current implementation. I have a Gale-Shapley algorithm based on two structures. But now I am facing the challenge of having to call this code with instances that need to hold more information. That is why I am considering the possible restructure of the algorithm over classes/instances instead of structures.