standalone deriving

Stream: lean4

[Yakov Pechersky]

Is there standalone deriving, a la Haskell?

section

inductive Foo where
  | lt | eq | gt
deriving Inhabited, BEq

end

deriving Repr for Foo -- totally illegitimate syntax
``
For example, `Ordering` is defined in base Lean 4. I would like to have it have a `Repr Ordering` instance. Is there a way for me to generate it without defining it manually?

[Matej Penciak]

deriving instance Repr for Foo should work (assuming it can derive the instance)

[Yakov Pechersky]

Awesome, thanks!