Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-25 09:58 d9327e43

View on Github →

refactor(geometry/manifold/real_instances): use fact instead of lt_class (#2521) To define a manifold with boundary structure on the interval [x, y], typeclass inference needs to know that x < y. This used to be provided by the introduction of a dummy class lt_class. The new mechanism based on fact makes it possible to remove this dummy class.

Estimated changes