Rational numbers for implementing decision procedures. We should not confuse them with the Mathlib rational numbers.

structure Std.Internal.Rat : Type

• num : Int
• den : Nat

instance Std.Internal.instInhabitedRat : Inhabited Std.Internal.Rat

Equations

• Std.Internal.instInhabitedRat = { default := { num := default, den := default } }

instance Std.Internal.instBEqRat : BEq Std.Internal.Rat

instance Std.Internal.instDecidableEqRat : DecidableEq Std.Internal.Rat

instance Std.Internal.instToStringRat : ToString Std.Internal.Rat

instance Std.Internal.instReprRat : Repr Std.Internal.Rat

@[inline]

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

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

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

Equations

• a.isInt = (a.den == 1)

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

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

Equations

• a.mul b = { num := a.num.tdiv ↑(a.num.natAbs.gcd b.den) * b.num.tdiv ↑(a.den.gcd b.num.natAbs), den := b.den / a.num.natAbs.gcd b.den * (a.den / a.den.gcd b.num.natAbs) }

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

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

Equations

• a.div b = a.mul b.inv

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

Equations

• One or more equations did not get rendered due to their size.

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

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

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

Equations

• a.floor = if (a.den == 1) = true then a.num else let r := a.num.tmod ↑a.den; if a.num < 0 then r - 1 else r

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

instance Std.Internal.Rat.instLT : LT Std.Internal.Rat

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

instance Std.Internal.Rat.instLE : LE Std.Internal.Rat

Equations

• Std.Internal.Rat.instLE = { le := fun (a b : Std.Internal.Rat) => ¬b < a }

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

Equations

• a.instDecidableLe b = inferInstanceAs (Decidable ¬b < a)

instance Std.Internal.Rat.instAdd : Add Std.Internal.Rat

Equations

• Std.Internal.Rat.instAdd = { add := Std.Internal.Rat.add }

instance Std.Internal.Rat.instSub : Sub Std.Internal.Rat

instance Std.Internal.Rat.instNeg : Neg Std.Internal.Rat

Equations

• Std.Internal.Rat.instNeg = { neg := Std.Internal.Rat.neg }

instance Std.Internal.Rat.instMul : Mul Std.Internal.Rat

Equations

• Std.Internal.Rat.instMul = { mul := Std.Internal.Rat.mul }

instance Std.Internal.Rat.instDiv : Div Std.Internal.Rat

Equations

• Std.Internal.Rat.instDiv = { div := fun (a b : Std.Internal.Rat) => a * b.inv }

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

Equations

• Std.Internal.Rat.instOfNat = { ofNat := { num := ↑n, den := 1 } }

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