Rational numbers for implementing decision procedures. We should not confuse them with the Batteries rational numbers, also used by Mathlib.

structure Std.Internal.Rat : Type

• num : Int
• den : Nat

instance Std.Internal.instInhabitedRat : Inhabited Rat

instance Std.Internal.instBEqRat : BEq Rat

instance Std.Internal.instDecidableEqRat : DecidableEq Rat

instance Std.Internal.instToStringRat : ToString Rat

instance Std.Internal.instReprRat : Repr Rat

@[inline]

def Std.Internal.Rat.normalize (a : Rat) : Rat

def Std.Internal.mkRat (num : Int) (den : Nat) : Rat

def Std.Internal.Rat.isInt (a : Rat) : Bool

def Std.Internal.Rat.lt (a b : Rat) : Bool

def Std.Internal.Rat.mul (a b : Rat) : Rat

def Std.Internal.Rat.inv (a : Rat) : Rat

def Std.Internal.Rat.div (a b : Rat) : Rat

def Std.Internal.Rat.add (a b : Rat) : Rat

def Std.Internal.Rat.sub (a b : Rat) : Rat

def Std.Internal.Rat.neg (a : Rat) : Rat

def Std.Internal.Rat.floor (a : Rat) : Int

def Std.Internal.Rat.ceil (a : Rat) : Int

instance Std.Internal.Rat.instLT : LT Rat

instance Std.Internal.Rat.instDecidableLt (a b : Rat) : Decidable (a < b)

instance Std.Internal.Rat.instLE : LE Rat

instance Std.Internal.Rat.instDecidableLe (a b : Rat) : Decidable (a ≤ b)

instance Std.Internal.Rat.instAdd : Add Rat

instance Std.Internal.Rat.instSub : Sub Rat

instance Std.Internal.Rat.instNeg : Neg Rat

instance Std.Internal.Rat.instMul : Mul Rat

instance Std.Internal.Rat.instDiv : Div Rat

instance Std.Internal.Rat.instOfNat {n : Nat} : OfNat Rat n

instance Std.Internal.Rat.instCoeInt : Coe Int Rat