Lean4
/-- Some definitions that define objects of a class cannot be instances, because they have an
explicit argument that does not occur in the conclusion. An example is `Preorder.lift` that has a
function `f : α → β` as an explicit argument to lift a preorder on `β` to a preorder on `α`.
If these definitions are used to define instances of this class *and* this class is an argument to
some other type-class so that type-class inference will have to unfold these instances to check
for definitional equality, then these definitions should be marked `@[reducible]`.
For example, `Preorder.lift` is used to define `Units.Preorder` and `PartialOrder.lift` is used
to define `Units.PartialOrder`. In some cases it is important that type-class inference can
recognize that `Units.Preorder` and `Units.PartialOrder` give rise to the same `LE` instance.
For example, you might have another class that takes `[LE α]` as an argument, and this argument
sometimes comes from `Units.Preorder` and sometimes from `Units.PartialOrder`.
Therefore, `Preorder.lift` and `PartialOrder.lift` are marked `@[reducible]`.
-/
def «reducible non-instances» : LibraryNote✝ :=
()
