Turn `IsLexicographicallyLess` into an obsolete synonym for `\<`#4504

Merged

ThomasBreuer merged 2 commits intogap-system:masterfrom fingolfin:mh/IsLexicographicallyLess

May 21, 2021

+35-51

Commits on May 20, 2021

Turn IsLexicographicallyLess into synonym for \<
fingolfin
committed

Commits on May 21, 2021

Mark IsLexicographicallyLess as deprecated
fingolfin
committed