code.lol / bytes

Init.Grind.Ordered.Rat

`grind` instances for `Rat` as an ordered module. #

instance Lean.Grind.instIsLinearOrderRat :

Std.IsLinearOrder Rat

instance Lean.Grind.instLawfulOrderLTRat :

Std.LawfulOrderLT Rat

instance Lean.Grind.instOrderedAddRat :

instance Lean.Grind.instOrderedRingRat :

OrderedRing Rat