Documentation

Init.Grind.Ordered.Int

grind instances for Int as an ordered module. #

source
instance Lean.Grind.instPreorderInt :
Preorder Int
Equations
    source
    instance Lean.Grind.instIsOrderedInt :
    IntModule.IsOrdered Int
    source
    instance Lean.Grind.instIsOrderedInt_1 :
    Ring.IsOrdered Int