# Documentation

## Lean.Data.Rat

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

structure Lean.Rat :
Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instReprRat :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
• a.normalize = let n := a.num.natAbs.gcd a.den; if (n == 1) = true then a else { num := a.num.div n, den := a.den / n }
Instances For
def Lean.mkRat (num : Int) (den : Nat) :
Equations
• Lean.mkRat num den = if (den == 0) = true then { num := 0, den := 1 } else { num := num, den := den }.normalize
Instances For
Equations
• a.isInt = (a.den == 1)
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• a.mul b = let g1 := a.den.gcd b.num.natAbs; let g2 := a.num.natAbs.gcd b.den; { num := a.num.div g2 * b.num.div g1, den := b.den / g2 * (a.den / g1) }
Instances For
Equations
• a.inv = if a.num < 0 then { num := -a.den, den := a.num.natAbs } else if (a.num == 0) = true then a else { num := a.den, den := a.num.natAbs }
Instances For
Equations
• a.div b = a.mul b.inv
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• a.neg = { num := -a.num, den := a.den }
Instances For
Equations
• a.floor = if (a.den == 1) = true then a.num else let r := a.num.mod a.den; if a.num < 0 then r - 1 else r
Instances For
Equations
• a.ceil = if (a.den == 1) = true then a.num else let r := a.num.mod a.den; if a.num > 0 then r + 1 else r
Instances For
instance Lean.Rat.instLT :
Equations
Equations
instance Lean.Rat.instLE :
Equations
Equations
instance Lean.Rat.instDiv :
Equations
instance Lean.Rat.instOfNat {n : Nat} :
Equations
• Lean.Rat.instOfNat = { ofNat := { num := n, den := 1 } }
Equations