Zulip Chat Archive

Stream: general

Topic: Extending classes vs. instance chaining


Donald Sebastian Leung (Mar 06 2020 at 15:01):

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 (Mar 06 2020 at 16:42):

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

Johan Commelin (Mar 06 2020 at 17:13):

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


Last updated: Dec 20 2023 at 11:08 UTC