Extending classes vs. instance chaining

Stream: general

[Donald Sebastian Leung]

Suppose I've formalized the axioms to incidence geometry as a typeclass in Lean and I now want to formalize the axioms to affine incidence geometry (incidence + parallel postulate). Which of the following is considered more elegant: 1) using extends on a class or 2) define the entire class from scratch and use instance chaining to derive a typeclass instance for incidence geometry given any affine incidence geometry?

[Reid Barton]

I don't know what instance chaining but it sounds like a way to manually achieve the same result as 1

[Johan Commelin]

@Donald Sebastian Leung I guess that (1) is the way to go.