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

structure Lean.Rat : Type

• num : Int
• den : Nat

instance Lean.instInhabitedRat : Inhabited Lean.Rat

Equations

• Lean.instInhabitedRat = { default := { num := default, den := default } }

instance Lean.instBEqRat : BEq Lean.Rat

Equations

• Lean.instBEqRat = { beq := Lean.beqRat✝ }

instance Lean.instDecidableEqRat : DecidableEq Lean.Rat

Equations

• Lean.instDecidableEqRat = Lean.decEqRat✝

instance Lean.instToStringRat : ToString Lean.Rat

Equations

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

instance Lean.instReprRat : Repr Lean.Rat

Equations

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

@[inline]

def Lean.Rat.normalize (a : Lean.Rat) : Lean.Rat

Equations

• Lean.Rat.normalize a = let n := Nat.gcd (Int.natAbs a.num) a.den; if (n == 1) = true then a else { num := Int.div a.num ↑n, den := a.den / n }

def Lean.mkRat (num : Int) (den : Nat) : Lean.Rat

Equations

• Lean.mkRat num den = if (den == 0) = true then { num := 0, den := 1 } else Lean.Rat.normalize { num := num, den := den }

def Lean.Rat.isInt (a : Lean.Rat) : Bool

Equations

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

def Lean.Rat.lt (a : Lean.Rat) (b : Lean.Rat) : Bool

Equations

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

def Lean.Rat.mul (a : Lean.Rat) (b : Lean.Rat) : Lean.Rat

Equations

• Lean.Rat.mul a b = let g1 := Nat.gcd a.den (Int.natAbs b.num); let g2 := Nat.gcd (Int.natAbs a.num) b.den; { num := Int.div a.num ↑g2 * Int.div b.num ↑g1, den := b.den / g2 * (a.den / g1) }

def Lean.Rat.inv (a : Lean.Rat) : Lean.Rat

Equations

• Lean.Rat.inv a = if a.num < 0 then { num := -↑a.den, den := Int.natAbs a.num } else if (a.num == 0) = true then a else { num := ↑a.den, den := Int.natAbs a.num }

def Lean.Rat.div (a : Lean.Rat) (b : Lean.Rat) : Lean.Rat

Equations

• Lean.Rat.div a b = Lean.Rat.mul a (Lean.Rat.inv b)

def Lean.Rat.add (a : Lean.Rat) (b : Lean.Rat) : Lean.Rat

Equations

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

def Lean.Rat.sub (a : Lean.Rat) (b : Lean.Rat) : Lean.Rat

Equations

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

def Lean.Rat.neg (a : Lean.Rat) : Lean.Rat

Equations

• Lean.Rat.neg a = { num := -a.num, den := a.den }

def Lean.Rat.floor (a : Lean.Rat) : Int

Equations

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

def Lean.Rat.ceil (a : Lean.Rat) : Int

Equations

• Lean.Rat.ceil a = if (a.den == 1) = true then a.num else let r := Int.mod a.num ↑a.den; if a.num > 0 then r + 1 else r

instance Lean.Rat.instLTRat : LT Lean.Rat

Equations

• Lean.Rat.instLTRat = { lt := fun (a b : Lean.Rat) => Lean.Rat.lt a b = true }

instance Lean.Rat.instDecidableLtRatInstLTRat (a : Lean.Rat) (b : Lean.Rat) : Decidable (a < b)

Equations

• Lean.Rat.instDecidableLtRatInstLTRat a b = inferInstanceAs (Decidable (Lean.Rat.lt a b = true))

instance Lean.Rat.instLERat : LE Lean.Rat

Equations

• Lean.Rat.instLERat = { le := fun (a b : Lean.Rat) => ¬b < a }

instance Lean.Rat.instDecidableLeRatInstLERat (a : Lean.Rat) (b : Lean.Rat) : Decidable (a ≤ b)

Equations

• Lean.Rat.instDecidableLeRatInstLERat a b = inferInstanceAs (Decidable ¬b < a)

instance Lean.Rat.instAddRat : Add Lean.Rat

Equations

• Lean.Rat.instAddRat = { add := Lean.Rat.add }

instance Lean.Rat.instSubRat : Sub Lean.Rat

Equations

• Lean.Rat.instSubRat = { sub := Lean.Rat.sub }

instance Lean.Rat.instNegRat : Neg Lean.Rat

Equations

• Lean.Rat.instNegRat = { neg := Lean.Rat.neg }

instance Lean.Rat.instMulRat : Mul Lean.Rat

Equations

• Lean.Rat.instMulRat = { mul := Lean.Rat.mul }

instance Lean.Rat.instDivRat : Div Lean.Rat

Equations

• Lean.Rat.instDivRat = { div := fun (a b : Lean.Rat) => a * Lean.Rat.inv b }

instance Lean.Rat.instOfNatRat {n : Nat} : OfNat Lean.Rat n

Equations

• Lean.Rat.instOfNatRat = { ofNat := { num := ↑n, den := 1 } }

instance Lean.Rat.instCoeIntRat : Coe Int Lean.Rat

Equations

• Lean.Rat.instCoeIntRat = { coe := fun (num : Int) => { num := num, den := 1 } }