Create a type class instance

3/4 ~25 minlean

Define `Named`, then provide an instance for `User`.

8 lines · Lean 4

class Named (α : Type) where
  name : α → String

structure User where
  login : String

instance : Named User where
  name := sorry

Objectifs

Indices

Voir la solution

class Named (α : Type) where
  name : α → String

structure User where
  login : String

instance : Named User where
  name := fun u => u.login